Skip to content

@AxiomMath AxiomMath

Change the repository type filter

All

    Repositories list

    39 repositories

    • RR_a3

      Public
      Lean
      •
      MIT License
      •0•1•0•0•Updated Aug 24, 2026Aug 24, 2026

    • PrimeGapsLib

      Public
      Lean formalization of bounded gaps between primes
      Lean
      •
      Apache License 2.0
      •5•36•2•2•Updated Aug 18, 2026Aug 18, 2026

    • EvenExponentDihedralMonotonicity

      Public
      Lean
      •
      Apache License 2.0
      •0•0•0•0•Updated Aug 17, 2026Aug 17, 2026

    • PaucityLatticeTriangle

      Public
      Lean
      •
      Other
      •0•0•0•0•Updated Aug 16, 2026Aug 16, 2026

    • QSeriesLib

      Public
      Lean Formalization of Everything about q-Series
      Lean
      •0•1•0•0•Updated Aug 16, 2026Aug 16, 2026

    • HJOa3Small

      Public
      Small cases of HJO at a=3
      Lean
      •
      Apache License 2.0
      •0•0•0•0•Updated Aug 16, 2026Aug 16, 2026

    • axle-mcp-server

      Public
      MCP Server for AI agents to interact with our Lean infrastructure
      Python
      •
      MIT License
      •2•37•0•1•Updated Aug 12, 2026Aug 12, 2026

    • axiom-lean-engine

      Public
      Lean evaluation and metaprogramming utilities for provers.
      Python
      •
      MIT License
      •19•150•1•0•Updated Aug 12, 2026Aug 12, 2026

    • RogersRamanujan

      Public
      Lean
      •3•6•0•0•Updated Aug 6, 2026Aug 6, 2026

    • BerkovichUncu

      Public
      Lean formalizations for the paper "A bijective proof of a partition theorem of Berkovich and Uncu"
      lean4
      lean4
      Lean
      •
      MIT License
      •0•1•0•0•Updated Aug 6, 2026Aug 6, 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
      •0•0•0•0•Updated Aug 5, 2026Aug 5, 2026

    • PrimeNumberTheoremAnd

      Public
      Axiom fork of https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
      Lean
      •
      Apache License 2.0
      •2•0•0•1•Updated Jul 29, 2026Jul 29, 2026

    • IMO2026

      Public
      Lean
      •
      MIT License
      •14•102•0•1•Updated Jul 17, 2026Jul 17, 2026

    • LatentError

      Public
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jul 15, 2026Jul 15, 2026

    • record-compositions

      Public
      Lean formalizations for the paper "Record compositions of alternating permutations and noncommutative symmetric functions"
      lean4
      lean4
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jul 15, 2026Jul 15, 2026

    • RogersRamanujan-artifacts

      Public
      Artifacts for "Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond"
      lean4
      lean4
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jul 13, 2026Jul 13, 2026

    • PartitionElliptic

      Public
      TeX
      •
      MIT License
      •0•1•0•0•Updated Jul 13, 2026Jul 13, 2026

    • HigherDyson

      Public
      TeX
      •
      MIT License
      •0•1•0•0•Updated Jul 8, 2026Jul 8, 2026

    • TanArctan

      Public
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jul 6, 2026Jul 6, 2026

    • erdos-public

      Public
      Axiom artifacts related to Erdős problems
      lean4
      lean4
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jun 18, 2026Jun 18, 2026

    • zeta-h123

      Public
      Lean formalizations for the paper "Thakur's hypotheses on power sums over $\mathbb{F}_q[t]$"
      lean4
      lean4
      Lean
      •
      MIT License
      •1•1•0•0•Updated Jun 16, 2026Jun 16, 2026

    • kaprekar4

      Public
      Lean formalizations for the paper "Four-digit Kaprekar dynamics in odd bases"
      lean4
      lean4
      Lean
      •
      MIT License
      •1•1•0•0•Updated Jun 11, 2026Jun 11, 2026

    • PartitionPolynomial

      Public
      Lean formalizations for the paper "Reciprocals of Partition Polynomials"
      Lean
      •
      MIT License
      •0•2•0•0•Updated Jun 8, 2026Jun 8, 2026

    • andrews_dhar_problem

      Public
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jun 8, 2026Jun 8, 2026

    • challenge_3

      Public
      Lean
      •
      MIT License
      •0•1•0•0•Updated Jun 5, 2026Jun 5, 2026

    • AgreeToDisagree

      Public
      Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"
      lean4
      lean4
      Lean
      •
      MIT License
      •3•22•0•0•Updated May 27, 2026May 27, 2026

    • Biswal

      Public
      Lean
      •
      MIT License
      •0•1•0•0•Updated Apr 29, 2026Apr 29, 2026

    • axplorer

      Public
      Jupyter Notebook
      •
      Apache License 2.0
      •28•182•0•1•Updated Apr 24, 2026Apr 24, 2026

    • ramanujan-tau-misses-primes

      Public
      Lean formalizations for the paper "ABC implies that Ramanujan's Tau function misses almost all primes"
      mathlean4
      mathlean4
      Lean
      •
      MIT License
      •5•12•0•0•Updated Apr 23, 2026Apr 23, 2026

    • axolver

      Public
      Jupyter Notebook
      •
      Apache License 2.0
      •5•10•0•0•Updated Apr 21, 2026Apr 21, 2026
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.