Thomas Kahle on Nostr: It’s slightly more complicated than this. There was also a lot of reinforcement ...

It’s slightly more complicated than this. There was also a lot of reinforcement learning on logical arguments. Because they can check the validity of an argument produced by an LLM with the proof checker lean, they could systematically train to make the LLM produce more valid arguments (with higher likelihood).

And coding agents also play a big role in this. They also trained on the tool use and sequences of commands a mathematician would type into the computer when doing research.

The progress in 2026 is mindblowing.