I've tripped across the new starup answer.ai. It seems their goal is to make it easier
to construct AI-based applications.<p>I'm looking at using AI to construct mathematical proofs.<p>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.<p>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.<p>How do I teach a foundation model to handle proof notation?