Can an entire Lean proof be read as a geometric object? An interactive first experiment, a carefully separated syntax graph and mathematical argument, and a research program for navigating formal proofs at different scales.
A dark dust clump can already contain a young star. What can survey data actually tell us—and what would it take to observe a stellar birth?
An interactive guide to the geometry of motion in the plane: from a simple constraint to the pendulum, competing routes, and the complete shortest-path solution.
One research program, three questions: when a path loses local optimality, where nearby paths focus, and how many paths reach the same position and heading. Follow the pendulum, explore the conjugate locus, and count the inverse images.
