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.
