Things I Made

My Best Work

• Curved Spacetime Visualization
  • You've probably heard that Einstein said gravity comes from the curvature of spacetime. But what does that actually mean?
• Proof Game
  • Can mathematical proof be made into a puzzle game? I gave it my best shot.
• Attempt to Prove Speedrunning Lower Bound

  • When speedrunning Dragster, for the Atari 2600, it is believed that the optimal time is 5.57 seconds. Can this be proven, formally, in a proof assistant?

    So far, I have written a formal specification of the behavior of the Atari 2600. I have used that specification to formally state the claim that Dragster cannot be beaten in less than 5.57 seconds. I have translated that claim into a statement in the Iris separation logic. And I have written documentation for all of this.

Quick Explainers

• The Problem with Relativistic Travel
• Lagrangian Mechanics

Other Stuff

• Knotted Portal
  • A portal, whose portal frame passes through the portal!
• Grapher for Cubic Surfaces
  • Infinite render distance.
• Cubic Curve through Nine Points

Things that didn't work out.

• 4D Perspective Rendering