Solve translates mathematical proofs into Lean, tests them, finetunes itself, and tries again.
Running time
Total attempts
Proofs written
24h success rate
The rise of large language models has sparked extraordinary advances in reasoning, code generation, and even mathematical problem-solving. But when it comes to formal logic, provable guarantees, and autonomous discovery LLMs fall short.
At Eigenform, we’re building something fundamentally different: a self-improving diffusion model that constructs and tests hypotheses using rigorous formal language like Lean: reasoning not simulating reasoning, with formal verification and adaptive feedback loops at its core.
Eigenform is a deep tech AI research organization dedicated to pioneering foundational technologies that push beyond conventional AI limitations.
Our models and agents consistently evolve through cycles of goal-setting, strategy implementation, rigorous evaluation, and adaptive learning.
Current LLMs inherit the ceiling of their training sets.
Our agents generate and validate brand-new knowledge – and hence high-entropy data – directly in their environment, guided by an unbounded, ungameable numeric reward, then use the new knowledge to fine-tune themselves.
Open Source Core – Fork on GitHub
Docs & Examples – Deep dives + quick starts
Community Discord – Peer support & research collabs
| Stage | Focus | Status |
|---|---|---|
| Self-Reasoning | Auto hypothesis & code generation (noprop strategies, incremental retraining) |
Live |
| Self-Assessment | Empirical validation frameworks | Live |
| Continuous Self-Improvement |
Sliding Window SFT, persistent memory, adaptive retraining | Live |
| Cross-Domain Generalisation |
Meta-learning, transfer learning methodologies | In development |
| Autonomous Evolution |
Self-directed R&D, exploratory innovation | Long-term |
