A Two-Stage System from a Peking University Team: Planning an Algebra Problem in Natural Language and Locking It In with Lean 4
By combining a component that generates mathematical strategy with a second component that carries the proof into a formal language, the researchers propose a two-track defense against the reliability weakness of large language models. The work is at the preprint stage; still, it offers a concrete example of how automated theorem proving and literature search can scale together.
AILLMTechnology
