A Two-Stage System from a Peking University Team: Planning an Algebra Problem in Natural Language and Locking It In with Lean 4
Originally published in Turkish. Read the original →
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.
In mathematics, the word "solution" only gains its weight when every step is tied into an auditable chain. That's exactly why it's drawing attention that a research group around Peking University (the team referred to in the press as led by Dong Bin) recently announced that it had closed an algebra problem, introduced into the literature by American mathematician Dan Anderson in 2014 and said to have remained open for a long time, using a workflow in which human intervention was kept to a minimum. The findings are only in preprint channels for now, so the final word will come from the peer-review process. Even so, the architecture described clearly lays out lessons about what AI should lean on in mathematics.
The problem isn't just "producing an answer"
Large language models are fluent in long texts; but fluency doesn't mean correctness. Especially in fields like abstract algebra, a single slipped symbol can invalidate an entire proof. That's why, instead of a single "magic chat," the researchers describe a two-layer design: first the method and research plan, then the translation of this plan into a language checked by a machine.
This separation carries a different motivation from classic computer algebra tools. The goal isn't just to simplify an equation; it's to scan the techniques accumulated in the literature, propose a new strategy and have every step of that strategy re-verified by another system.
A two-component pipeline: intuition and locking in
In the framework that was shared, the first component (the part referred to in the news coverage as "Rethlas") takes on a role resembling mathematicians' day-to-day work: scanning the library and drawing up a roadmap, sequencing attempts, linking intermediate results together. The second component, the layer referred to as "Archon," pours this roadmap into a concrete formal skeleton in an interactive theorem prover environment, namely the Lean 4 ecosystem. Because the Lean side speaks in syntax and type rules rather than "nice prose," the idea the model generates enters a hard filter here.
This dual structure doesn't eliminate the risk of hallucination; but it increases the chance of catching an error at the moment of generation. If a claim produced in natural language doesn't compile on the formal side, the process doesn't move forward; so the cost of an error is paid early.
Timescale and the automation claim
The statements say the work took about eighty hours and that most of this time was run by the machine. Such durations aren't miraculous on their own; but bringing literature search, trial and error and formalization into the same pipeline may be compressing work that could take months if done by hand. The real issue here isn't speed itself but the emergence of a repeatable template: whether the same pipeline can be adapted to problems of a similar class.
The discipline of working with non-peer-reviewed texts
The fact that the findings haven't yet passed traditional peer review fuels excitement but also makes cautious reading mandatory. A preprint is the fast channel of scientific communication; but its error-correction mechanism works more slowly. The technical details described in this post should be positioned as "the reported design" rather than "established fact." Still, the methodological discussion is valuable on its own: connecting tools like Lean to AI pipelines can be thought of as a mathematical variant of the "model + verifier" pair we see in safety-critical software in industry.
Practical takeaways for mathematicians
From a researcher's or engineer's perspective, three conclusions stand out:
1. Formal tools are no longer helpers but a verification layer. Even though Lean 4 has a steep learning curve, it is becoming a direct integration target for securing generated ideas. 2. When literature access is combined with automation, new kinds of discovery open up. The model isn't a genius on its own; but it can be positioned like a "parallel intern" that can quickly try connections a human might miss. 3. Human oversight doesn't end; it moves. Even if the process looks autonomous end to end, which axioms are accepted, which libraries are trusted and which formal translation is made remain tied to the framework a human sets up.
Fast generation, slow confirmation
AI has sped up the "conversation" in mathematics; Lean-like systems offer the chance to turn that conversation into something signed off by a "notary." The lasting impact of this story will be measured less by a single problem being solved in record time than by similar pipelines becoming standard in academia and the software world. Until a peer-reviewed publication arrives, the results should be read with caution; but the architectural idea gives a clear answer to the question already at the door: in advanced reasoning, verification doesn't chase after generation; it constrains and shapes it at the same time.
