Projects

Completed or Significant Progress

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.

Idea Stage

Graphing Calculator with Quantifiers

I'd like to make a graphing calculator, analogous to Desmos, that supports quantifiers. For instance, you could ask for a graph of \(\exists t, (t-x)^2 + (t^3-y)^2 \leq 0.1^2\), and it would plot the region within distance 0.1 of the cubic \(y = x^3\).

If we limit the calculator to work with polynomials, this is possible, using the algorithm of quantifier elimination by cylindrical algebraic decomposition. This limitation is necessary; if we allow trig functions, the problem is undecidable. If we add exponentials, decidability is unknown. (Source)

Unfortunately, quantifier elimination is complicated and slow. It may be necessary to use an existing implementation, rather than implementing it myself, and I am unsure whether any existing implementations can be run inside a web application.