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 →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
A taste of the maths
Four real theorems — one for each roadmap theme — extracted from the library and type-checked when this page is built, so they cannot drift out of date.
open TauCeti in
/-- Universal covers — two deck transformations of a connected covering space that
agree at a single point of the total space are equal. -/
theorem deck_rigidity {E B : Type*} [TopologicalSpace E] [TopologicalSpace B]
{p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p)
(φ ψ : Deck p) {e : E} (h : φ.1 e = ψ.1 e) : φ = ψ :=
Deck.eq_of_apply_eq hp φ ψ hopen TauCeti.PDE Matrix in
/-- Partial differential equations — on a uniformly elliptic region the coefficient
matrix induces a coercive bilinear form, the hypothesis that powers Lax–Milgram. -/
theorem ellipticity_coercive {X n : Type*} [Fintype n] [DecidableEq n]
{Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ}
(h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) :
IsCoercive (matrixBilinearForm (a x)) :=
h.isCoercive_matrixBilinearForm hxopen TauCeti.AlgebraicGeometry TauCeti.AlgebraicGeometry.WeilDivisor in
/-- The Jacobian challenge — a nonzero effective Weil divisor has a point with
strictly positive coefficient. -/
theorem effective_divisor {X : Type*} {D : WeilDivisor X}
(hD : IsEffective D) (hD0 : D ≠ 0) : ∃ x, 0 < D.coeff x :=
hD.exists_pos_coeff_of_ne_zero hD0open HopfAlgebra in
/-- Reductive algebraic groups — a bialgebra homomorphism between Hopf algebras
commutes with the antipodes. -/
theorem hopf_antipode {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
[HopfAlgebra R A] [HopfAlgebra R B] (φ : A →ₐc[R] B) :
φ.toLinearMap.comp (antipode R (A := A)) = (antipode R (A := B)).comp φ.toLinearMap :=
TauCeti.BialgHom.toLinearMap_comp_antipode φ