Just met with an old college friend who I haven't seen in a decade. He just got his PhD in Physics last December and now is part of a organization building and using a very interesting MCP (called Ax Prover) that acts as a proof-assistant (and eventually a formalization tool - to build out a database of formalized proofs) using the Lean language/proof assistant He's helping extend the library to formalize quantum mechanics proofs.
The idea is that it can expedite (exponentially) math and mathematical science research.
All it incorporates is an MCP. There is no distillation or fine-tuning.
Eventually these extended databases can be used to improve reinforcement learning in the vein of AlphaGeometry or AlphaProof.
These are the sort of tools we're heading toward. Less about the base model and more about neuro-symbolic systems with LLMs as sub-components.
https://arxiv.org/abs/2510.12787
