Automatically Generalizing Math

2026-01-02

The experience I’m imagining is writing a proof which only applies to a single context, e.g. a proof in which you explicitly work in the hyperbolic plane but which could work for any Riemannian manifold could be instantly generalized.

For an implementation, I imagine something like typeclasses and Haskell type system could automatically generalize mathematical proofs. Silly example: you only apply group axioms, then your theorem/function (perhaps the connection between functions and theorems could be made explicit via Curry-Howard) is of type (Group) G => type…

If you know about a project that sounds like this, please send me an email.