Inspirations

Slean did not come from nowhere. Here is what we borrow from each source, and what we do not claim.

Lean and Mathlib

Lean is a programming language and proof assistant: a small kernelLean kernel Lean is software that checks mathematical proofs. Its kernel is a small program that checks every step. If it accepts, the proof is correct, without taking anyone’s word for it. checks every proof. Mathlib is its shared mathematics library.

• What we borrow: kernel-checked proofs, a shared library that accumulates, and an explicit frontier of statements still open. Slean is Science + Lean.
• What we do not claim: Slean is not a new formal language, and a law proved in a simulated world is not a theorem about nature.

Physlib

Physlib formalises physics in Lean.

• What we borrow: its definitions, which Slean will reuse for physics worlds (milestone M4 on the roadmap) rather than duplicate them.
• What we do not claim: Slean does not replace Physlib and has not used it yet.

Wolfram Physics Project

The Wolfram Physics Project explores the space of simple rules and looks for emergent structure.

• What we borrow: the method: enumerate rules, simulate, look for regularities.
• What we do not claim: we do not adopt its conclusions, which have no accepted testable prediction yet.

Minimo

“Learning Formal Mathematics From Intrinsic Motivation”, Poesia, Broman, Haber and Goodman, NeurIPS 2024 (arXiv 2407.00695): an agentagent An AI program that works on its own: it runs experiments, proposes claims and reads the verifier’s answers. that poses its own conjectures and proves them from axioms alone.

• What we borrow: the idea of open-ended exploration without a fixed target.
• What we do not claim: Slean does not do open-ended discovery yet; its agents answer prescribed kinds of claims.

STP

“Self-play LLM Theorem Provers with Iterative Conjecturing and Proving”, Dong and Ma, ICML 2025 (paper): a conjecturer and a prover training each other in Lean.

• What we borrow: the propose-and-verify pair, where the exact verifier gives the signal.
• What we do not claim: Slean does not train models today.

Dream-RSI

“Recursive Self-Improvement through Evolving Worlds”, Zheng et al., 2026 (arXiv 2609.14858): replaying recorded discovery trees to improve the exploration policy cheaply.

• What we borrow: the idea of keeping every exploration so it can be replayed. That needs deterministic scores, which Slean’s exact verifier provides.
• What we do not claim: Slean has not built this improvement loop yet.

Karpathy’s autoresearch loop

Andrej Karpathy’s autoresearch loop, propose, run, keep or discard, is the lineage of Mutome’s engine. Slean provides the “keep or discard” step with an exact judge instead of an impression.

For more, see Slean in 5 minutes and Four kinds of evidence.