An AI research pipeline is now generating novel mathematical theorems, proving them formally, and using those proofs to get better at proving the next ones.
Researchers introduced a system called the Conjecturing-Proving Loop, or CPL, which runs inside Lean 4, a formal proof assistant where every logical step is machine-checked. The loop works in two alternating phases: an LLM proposes a mathematical conjecture, then attempts to prove it. If the proof checks out, that theorem-proof pair gets added to the model's context for the next iteration. No extra training, no fine-tuning — just the model reading its own verified track record before trying again.
The self-referential trick is what makes this worth paying attention to. Most neural theorem-proving systems generate statements and proofs in a single pass; CPL splits them, letting proof difficulty inform what gets conjectured next. The researchers found this separation meaningfully increases the discovery rate of theorems that are hard to prove — the ones that actually matter to mathematicians. The fact that a model's own formally verified outputs make it measurably better at subsequent tasks is a concrete data point for in-context learning doing real work, not just pattern-matching.
For context: formal verification has long been the gap between "the AI got the right answer" and "the AI can be trusted." Lean 4 closes that gap by rejecting any proof with a logical flaw. That CPL operates inside this constraint, rather than just generating plausible-looking math, puts it in different territory than most headline-grabbing AI-solves-math stories — though the gap between automated conjecture generation and Fields Medal-level insight remains considerable.