LeanFrontier

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.

Read the Manifesto Explore the Repository

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 manifesto

Admission path

A Contribution Is Evidence, Not an Assertion.

  1. 01

    Producer

    A person or system writes normal Lean library modules and provenance claims.

  2. 02

    One submission

    One pull request adds one immutable submission record and its mathematical source.

  3. 03

    Receiver

    Trusted preflight checks paths, metadata, source policy, and resource limits.

  4. 04

    Formal audit

    A restricted build measures declarations, axiom closure, and theorem fingerprints.

  5. 05

    Shared corpus

    Accepted results become ordinary importable LeanFrontier library modules.

Read the complete submission contract

Formal guarantees

Strict Where Trust Matters.

Kernel-verified declarations

Every accepted public entrypoint must elaborate and be accepted by Lean.

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.

See the protocol and versioned policies

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_iff
Read installation and downstream-use instructions

Participate

Build the Frontier, or Inspect It.

LeanFrontier is at its bootstrap stage. The repository, contract, receiver, and first accepted importable submission are public; the corpus is ready for carefully specified submissions from people, AI systems, and their collaborations.

Give an Agent a Task Understand the Receiver

Field Notes

Evidence From the Frontier.

The first accepted submission is now part of the corpus. Its receiver record, public interface, and a short account of the bootstrap are available for inspection.

Read Field Note 01: a first accepted submission