Kernel-verified declarations
Every accepted public entrypoint must elaborate and be accepted by Lean, and each submitted module is replayed through the kernel with leanchecker rather than admitted on the elaborator's word.
Lean 4 · machine mathematics · formal verification
A Frontier for Mathematics the Kernel Can Verify.
LeanFrontier is a public Lean 4 library for machine-generated mathematics. It makes one demand absolute: accepted declarations must pass a narrow, reproducible formal trust boundary.
The Governing Principle
Freedom Above the Kernel;
Rigidity Below It.
Machines may formulate statements, create definitions, and develop their own formal theories. The receiver does not require a human explanation of every proof. It does require mechanical evidence that each accepted result is valid within Lean’s explicit trust boundary.
The experiment
Let the Corpus Become an Object of Study.
Formal validity and human mathematical understanding are not the same condition. LeanFrontier explores what happens when machine systems can accumulate verified mathematics without being constrained by a human-curated theory of what is elegant, interesting, or easy to explain.
The result may reconnect with familiar mathematics, develop useful new structures, or expose sterile directions. The project is designed to measure that landscape rather than decide it in advance.
Read Freedom Above the Kernel, the complete manifestoAdmission path
A Contribution Is Evidence, Not an Assertion.
- 01
Producer
A person or system writes normal Lean library modules and provenance claims.
- 02
One submission
One pull request adds one immutable submission record and its mathematical source.
- 03
Receiver
Trusted preflight checks paths, metadata, source policy, and resource limits.
- 04
Formal audit
A restricted build replays the submitted modules through the kernel, then measures declarations, axiom closure, and theorem fingerprints.
- 05
Shared corpus
Accepted results become ordinary importable LeanFrontier library modules.
Formal guarantees
Strict Where Trust Matters.
Narrow axiom boundary
sorry, custom axioms, and unauthorized transitive axiom dependencies are rejected.
Reproducible receiver observations
Claims remain immutable; build and audit observations are emitted separately as reports.
Mechanical corpus hygiene
Duplicate, degenerate-family, baseline-triviality, and resource checks run before admission, counted against the whole accepted corpus rather than one submission.
Use the library
A Normal Lake Dependency.
LeanFrontier is intended to work like any ordinary Lean package: pin a revision, run Lake, and import exactly the library surface you need.
import Mathlib.Data.Complex.Basic
import LeanFrontier.Geometry.InversiveGeometry
open ComplexConjugate
open LeanFrontier.InversiveGeometry
#check reflect_eq_self_iffParticipate
Build the Frontier, or Inspect It.
LeanFrontier is early, and now open in practice as well as in principle: the repository, contract, receiver, and every accepted importable submission are public, and the corpus has admitted work from an outside contributor. It is ready for carefully specified submissions from people, AI systems, and their collaborations.
Field Notes
Evidence From the Frontier.
The corpus now spans ten subject areas, from inversive geometry and elementary number theory to interval dynamics, the Furstenberg topology, the plain changes rung on English tower bells since 1677, and a character sum proved without the commutativity its usual statement assumes. Their receiver records, public interfaces, and corpus patterns are available for inspection.
Read Field Note 05: a day spent attacking the receiver