Singularity

This is an automated archive made by the Lemmit Bot.

The original was posted on /r/singularity by /u/kaggleqrdl on 2025-11-13 02:09:30+00:00.

https://www.nature.com/articles/s41586-025-09833-y

Recent AI systems, often reliant on human data, typically lack the formal verification necessary to guarantee correctness. By contrast,  formal languages such as Lean1 offer an interactive environment that grounds reasoning, and reinforcement learning (RL) provides a mechanism for learning in such environments. We present AlphaProof, an AlphaZero-inspired2 agent that learns to find formal proofs through RL by training on millions of auto-formalized problems. 

Lean is cool because the AI can actually verify if it got the answer correct. Unlike other forms of learning, it can actually do RLVR, reinforcement learning with verifiable rewards.  

https://en.wikipedia.org/wiki/Lean/_(proof/_assistant)

A lot of people are working heavily in this area. math.inc and Terrence Tao is very interested in this. Great recent article in quanta suggesting a complimentary usage of SAT - https://www.quantamagazine.org/to-have-machines-make-math-proofs-turn-them-into-a-puzzle-20251110/ (weird photo spread of heule tho)