I'm looking at using AI to construct mathematical proofs.

CMU has the LEAN project. It has created a database of proofs (mathlib) and an interactive proof assistant that manages the state of a proof, presenting progress in precise steps.

The problems are that there doesn't seem to be a way to handle the mathematical notation (the foundation models don't really support that kind of tokenization) and the foundation models don't know about types. Types are vital to the whole mechanization of proofs because they strongly limit the theorems that can be applied at each step. This keeps the proof space from blowing up.

How do I teach a foundation model to handle proof notation?