A hexapus reaching toward an AI across a tide pool, beneath twin suns and a ringed planet.

Tau Ceti

Let’s do lots of maths.

AI-authored Lean mathematics, directed by a human-owned roadmap and gated by open, adversarial review.

Explore the code →Read the docs →

Humans own the roadmap

Mathematicians set the targets in a separate, human-reviewed roadmap repository. People choose the maths.

AIs write the code

AI agents author the Lean proofs and open pull requests — every theorem machine-checked, no sorries, no stray axioms.

Open review gates everything

AI reviewers judge each PR against fixed, open-source rubrics — correctness, reuse, API, naming, generality — before it can merge.

On the roadmap

Universal covers

The Jacobian challenge

Reductive algebraic groups

Partial differential equations

Growing fast

See the statistics →

Three repositories

TauCeti

The AI-authored Lean mathematics.

TauCetiRoadmap

The human-controlled roadmaps that direct the work.

TauCetiReview

The review rubrics and the machinery that runs review.

A taste of the maths

Burnside’s theorem, Carathéodory’s boundary extension theorem, and Schur–Weyl duality — each example is checked against the library when this page is built.

              open TauCeti in
/-- Burnside's theorem — every finite group of order pᵃqᵇ, for primes p and q,
is solvable. -/
theorem burnside {G : Type*} [Group G] [Finite G] {p q a b : ℕ}
    (hp : p.Prime) (hq : q.Prime) (h : Nat.card G = p ^ a * q ^ b) :
    Group.IsSolvable G :=
  isSolvable_of_card_eq_prime_pow_mul_prime_pow hp hq hopen TauCeti Set Metric Bornology in
/-- Carathéodory's boundary extension theorem — a Riemann map onto a Jordan
domain extends to a homeomorphism of the closures. -/
theorem caratheodory {Ω : Set ℂ}
    (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩb : IsBounded Ω)
    (hΩJ : IsJordanCurve (frontier Ω)) :
    ∃ g : ℂ → ℂ, ContinuousOn g (closedBall 0 1) ∧
      DifferentiableOn ℂ g (ball 0 1) ∧ BijOn g (ball 0 1) Ω ∧
      ∃ e : closedBall (0 : ℂ) 1 ≃ₜ closure Ω,
        ∀ z : closedBall (0 : ℂ) 1, (e z : ℂ) = g z :=
  exists_homeomorph_closedBall_closure_of_isJordanCurve_frontier hΩo hΩc hΩb hΩJopen TauCeti in
/-- Schur–Weyl duality — on the d-th tensor power of kⁿ, the images of the
general linear and symmetric group algebras are each other's centralizers. -/
theorem schur_weyl {k : Type*} [Field k] [Infinite k] {n d : ℕ}
    [NeZero (Nat.factorial d : k)] :
    Subalgebra.centralizer k (Set.range ⇑(tensorPowerRep k n d).asAlgebraHom) =
        (permTensorActionAlgHom k n d).range ∧
      Subalgebra.centralizer k (Set.range ⇑(permTensorActionAlgHom k n d)) =
        (tensorPowerRep k n d).asAlgebraHom.range :=
  ⟨centralizer_range_tensorPowerRep_asAlgebraHom_eq_range_permTensorActionAlgHom,
    centralizer_range_permTensorActionAlgHom_eq_range_tensorPowerRep_asAlgebraHom⟩