Repositories list

• AreaLaw2D

  Public

  AxiomMath/AreaLaw2D’s past year of commit activity
  Lean 4 formalization of OpenAI's 'A two-dimensional area law from a global spectral gap' (openai/math family 265): Theorem 1.1, every proposition, statement aud…

  Lean

  •

  Apache License 2.0

  •22 forks in AxiomMath/AreaLaw2D•00 stars in AxiomMath/AreaLaw2D•00 issues in AxiomMath/AreaLaw2D•11 pull request in AxiomMath/AreaLaw2D•Updated Oct 27, 2026Oct 27, 2026

• CFSG

  Public

  AxiomMath/CFSG’s past year of commit activity
  A Lean formalization of the Classification of Finite Simple Groups

  Lean

  •

  Apache License 2.0

  •1818 forks in AxiomMath/CFSG•146146 stars in AxiomMath/CFSG•00 issues in AxiomMath/CFSG•55 pull requests in AxiomMath/CFSG•Updated Oct 27, 2026Oct 27, 2026

• ClusterAlgebras

  Public
  Lean

  •

  Apache License 2.0

  •11 fork in AxiomMath/ClusterAlgebras•33 stars in AxiomMath/ClusterAlgebras•00 issues in AxiomMath/ClusterAlgebras•00 pull requests in AxiomMath/ClusterAlgebras•Updated Oct 27, 2026Oct 27, 2026

• nanoda

  Public

  AxiomMath/nanoda’s past year of commit activity
  Rust

  •

  Apache License 2.0

  •11 fork in AxiomMath/nanoda•11 star in AxiomMath/nanoda•00 issues in AxiomMath/nanoda•00 pull requests in AxiomMath/nanoda•Updated Oct 27, 2026Oct 27, 2026

• RiemannJensen

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/RiemannJensen•22 stars in AxiomMath/RiemannJensen•00 issues in AxiomMath/RiemannJensen•00 pull requests in AxiomMath/RiemannJensen•Updated Oct 23, 2026Oct 23, 2026

• CollatzPositiveDensity

  Public

  AxiomMath/CollatzPositiveDensity’s past year of commit activity
  Lean

  •

  Apache License 2.0

  •11 fork in AxiomMath/CollatzPositiveDensity•33 stars in AxiomMath/CollatzPositiveDensity•00 issues in AxiomMath/CollatzPositiveDensity•00 pull requests in AxiomMath/CollatzPositiveDensity•Updated Oct 23, 2026Oct 23, 2026

• PrimeNumberTheoremAnd

  Public

  AxiomMath/PrimeNumberTheoremAnd’s past year of commit activity
  Axiom fork of https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

  Lean

  •

  Apache License 2.0

  •44 forks in AxiomMath/PrimeNumberTheoremAnd•33 stars in AxiomMath/PrimeNumberTheoremAnd•00 issues in AxiomMath/PrimeNumberTheoremAnd•22 pull requests in AxiomMath/PrimeNumberTheoremAnd•Updated Oct 21, 2026Oct 21, 2026

• TernaryPoly

  Public

  AxiomMath/TernaryPoly’s past year of commit activity
  Lean formalization of ternary polynomial relations and periods of cusp forms

  Lean

  •

  Apache License 2.0

  •11 fork in AxiomMath/TernaryPoly•11 star in AxiomMath/TernaryPoly•00 issues in AxiomMath/TernaryPoly•00 pull requests in AxiomMath/TernaryPoly•Updated Oct 16, 2026Oct 16, 2026

• HigherDyson2

  Public

  AxiomMath/HigherDyson2’s past year of commit activity
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/HigherDyson2•00 stars in AxiomMath/HigherDyson2•00 issues in AxiomMath/HigherDyson2•00 pull requests in AxiomMath/HigherDyson2•Updated Oct 15, 2026Oct 15, 2026

• axiom-lean-engine

  Public
  Lean evaluation and metaprogramming utilities for provers.

  Python

  •

  MIT License

  •2525 forks in AxiomMath/axiom-lean-engine•176176 stars in AxiomMath/axiom-lean-engine•11 issue in AxiomMath/axiom-lean-engine•00 pull requests in AxiomMath/axiom-lean-engine•Updated Oct 14, 2026Oct 14, 2026

• lean-metrics

  Public
  Source and dependency-structure metrics for a Lean 4 Lake project

  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/lean-metrics•22 stars in AxiomMath/lean-metrics•00 issues in AxiomMath/lean-metrics•00 pull requests in AxiomMath/lean-metrics•Updated Oct 13, 2026Oct 13, 2026

• DedekindZetaZeroFree

  Public
  Lean 4 formalization of a uniform zero-free region for Dedekind zeta functions: ζ_K(s) ≠ 0 for Re(s) > 31/32

  Lean

  •

  Apache License 2.0

  •33 forks in AxiomMath/DedekindZetaZeroFree•66 stars in AxiomMath/DedekindZetaZeroFree•00 issues in AxiomMath/DedekindZetaZeroFree•00 pull requests in AxiomMath/DedekindZetaZeroFree•Updated Oct 13, 2026Oct 13, 2026

• HJO

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/HJO•22 stars in AxiomMath/HJO•00 issues in AxiomMath/HJO•00 pull requests in AxiomMath/HJO•Updated Oct 7, 2026Oct 7, 2026

• BSDTamagawa

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/BSDTamagawa•00 stars in AxiomMath/BSDTamagawa•00 issues in AxiomMath/BSDTamagawa•00 pull requests in AxiomMath/BSDTamagawa•Updated Oct 6, 2026Oct 6, 2026

• ZetaZerosV2

  Public
  Lean

  •

  Apache License 2.0

  •11 fork in AxiomMath/ZetaZerosV2•1111 stars in AxiomMath/ZetaZerosV2•00 issues in AxiomMath/ZetaZerosV2•00 pull requests in AxiomMath/ZetaZerosV2•Updated Oct 3, 2026Oct 3, 2026

• BondalThomsen

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/BondalThomsen•11 star in AxiomMath/BondalThomsen•00 issues in AxiomMath/BondalThomsen•00 pull requests in AxiomMath/BondalThomsen•Updated Oct 3, 2026Oct 3, 2026

• BGP212

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/BGP212•00 stars in AxiomMath/BGP212•00 issues in AxiomMath/BGP212•00 pull requests in AxiomMath/BGP212•Updated Oct 2, 2026Oct 2, 2026

• CycleCutoff

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/CycleCutoff•00 stars in AxiomMath/CycleCutoff•00 issues in AxiomMath/CycleCutoff•00 pull requests in AxiomMath/CycleCutoff•Updated Sep 29, 2026Sep 29, 2026

• Zeta5Irrational

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/Zeta5Irrational•00 stars in AxiomMath/Zeta5Irrational•00 issues in AxiomMath/Zeta5Irrational•00 pull requests in AxiomMath/Zeta5Irrational•Updated Sep 26, 2026Sep 26, 2026

• PrincipalComponentError

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/PrincipalComponentError•00 stars in AxiomMath/PrincipalComponentError•00 issues in AxiomMath/PrincipalComponentError•00 pull requests in AxiomMath/PrincipalComponentError•Updated Sep 21, 2026Sep 21, 2026

• axle-mcp-server

  Public
  MCP Server for AI agents to interact with our Lean infrastructure

  Python

  •

  MIT License

  •22 forks in AxiomMath/axle-mcp-server•3737 stars in AxiomMath/axle-mcp-server•00 issues in AxiomMath/axle-mcp-server•11 pull request in AxiomMath/axle-mcp-server•Updated Sep 16, 2026Sep 16, 2026

• BrowningSawin

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/BrowningSawin•00 stars in AxiomMath/BrowningSawin•00 issues in AxiomMath/BrowningSawin•00 pull requests in AxiomMath/BrowningSawin•Updated Sep 16, 2026Sep 16, 2026

• GranvilleMoore

  Public
  Lean

  •

  Apache License 2.0

  •00 forks in AxiomMath/GranvilleMoore•00 stars in AxiomMath/GranvilleMoore•11 issue in AxiomMath/GranvilleMoore•00 pull requests in AxiomMath/GranvilleMoore•Updated Sep 16, 2026Sep 16, 2026

• partial-regularity

  Public
  Lean formalizations for the paper "Almost all primes are partially regular"

  Lean

  •

  MIT License

  •11 fork in AxiomMath/partial-regularity•66 stars in AxiomMath/partial-regularity•00 issues in AxiomMath/partial-regularity•00 pull requests in AxiomMath/partial-regularity•Updated Sep 11, 2026Sep 11, 2026

• TanArctan

  Public
  Lean

  •

  MIT License

  •00 forks in AxiomMath/TanArctan•11 star in AxiomMath/TanArctan•00 issues in AxiomMath/TanArctan•00 pull requests in AxiomMath/TanArctan•Updated Sep 11, 2026Sep 11, 2026

• kaprekar4

  Public
  Lean formalizations for the paper "Four-digit Kaprekar dynamics in odd bases"

  lean4

  lean4

  Lean

  •

  MIT License

  •11 fork in AxiomMath/kaprekar4•11 star in AxiomMath/kaprekar4•00 issues in AxiomMath/kaprekar4•00 pull requests in AxiomMath/kaprekar4•Updated Sep 11, 2026Sep 11, 2026

• record-compositions

  Public
  Lean formalizations for the paper "Record compositions of alternating permutations and noncommutative symmetric functions"

  lean4

  lean4

  Lean

  •

  MIT License

  •00 forks in AxiomMath/record-compositions•11 star in AxiomMath/record-compositions•00 issues in AxiomMath/record-compositions•00 pull requests in AxiomMath/record-compositions•Updated Sep 11, 2026Sep 11, 2026

• QBinomialTrace

  Public
  Lean formalizations for the paper "On a conjecture of Han and Xiong for fractional Gaussian binomial coefficients"

  lean4

  lean4

  Lean

  •

  MIT License

  •00 forks in AxiomMath/QBinomialTrace•11 star in AxiomMath/QBinomialTrace•00 issues in AxiomMath/QBinomialTrace•00 pull requests in AxiomMath/QBinomialTrace•Updated Sep 11, 2026Sep 11, 2026

• PartitionElliptic

  Public
  TeX

  •

  MIT License

  •00 forks in AxiomMath/PartitionElliptic•11 star in AxiomMath/PartitionElliptic•00 issues in AxiomMath/PartitionElliptic•00 pull requests in AxiomMath/PartitionElliptic•Updated Sep 11, 2026Sep 11, 2026

• fel-polynomial

  Public
  Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"

  mathlean4

  mathlean4

  Lean

  •

  MIT License

  •44 forks in AxiomMath/fel-polynomial•4747 stars in AxiomMath/fel-polynomial•00 issues in AxiomMath/fel-polynomial•00 pull requests in AxiomMath/fel-polynomial•Updated Sep 11, 2026Sep 11, 2026