Repositories list

• Poincare-Conjecture

  Public
  Formalizing the Poincaré Conjecture in Lean 4

  Lean

  •

  Apache License 2.0

  •11 fork•55 stars•33 issues•00 pull requests•Updated Aug 17, 2026Aug 17, 2026

• Archon

  Public
  AI-assisted Lean project automation with DAG blueprints, proof orchestration, and multi-agent coding/proving workflows.

  automationtheorem-provingmathematics+ 9

  automationtheorem-provingmathematicsproof-assistantleanformal-methodsdagcodexai-agentsclaude+ 2

  Python

  •

  Apache License 2.0

  •3636 forks•199199 stars•00 issues•00 pull requests•Updated Aug 17, 2026Aug 17, 2026

• Danus

  Public
  Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

  mathematicsmulti-agentagents+ 5

  mathematicsmulti-agentagentscodexautomated-reasoningllmai4mathclaude-code

  Python

  •

  Apache License 2.0

  •4141 forks•185185 stars•00 issues•11 pull request•Updated Aug 12, 2026Aug 12, 2026

• iteris

  Public

  frenzymath/iteris’s past year of commit activity
  AI Agentic Research System for Computational Mathematics

  Python

  •

  Apache License 2.0

  •1212 forks•4545 stars•00 issues•11 pull request•Updated Aug 9, 2026Aug 9, 2026

• FormalPantheon

  Public

  frenzymath/FormalPantheon’s past year of commit activity
  A living, long-term archive that collects our formal project results across all domains.

  Lean

  •

  Apache License 2.0

  •00 forks•33 stars•00 issues•00 pull requests•Updated Aug 8, 2026Aug 8, 2026

• reap

  Public
  General neural tactic for Lean 4

  Lean

  •

  Apache License 2.0

  •33 forks•4343 stars•22 issues•11 pull request•Updated Aug 6, 2026Aug 6, 2026

• Rethlas_results

  Public
  Rethlas Results

  Creative Commons Attribution 4.0 International

  •11 fork•22 stars•00 issues•00 pull requests•Updated Aug 5, 2026Aug 5, 2026

• Rethlas

  Public
  Python

  •

  Apache License 2.0

  •4545 forks•285285 stars•44 issues•22 pull requests•Updated Aug 3, 2026Aug 3, 2026

• Archon-Horizon

  Public
  Workspace-first orchestration for long-horizon Lean 4 formalization agents.

  aidashboardtheorem-proving+ 13

  aidashboardtheorem-provingworkspaceorchestrationmulti-agentleanformalizationblueprintsagents+ 6

  Python

  •

  Apache License 2.0

  •00 forks•2020 stars•11 issue•00 pull requests•Updated Jul 30, 2026Jul 30, 2026

• jixia_py

  Public
  Python binding of jixia

  Python

  •22 forks•22 stars•00 issues•00 pull requests•Updated Jul 1, 2026Jul 1, 2026

• jixia

  Public
  A static analysis tool for Lean 4.

  Lean

  •

  Apache License 2.0

  •1313 forks•128128 stars•00 issues•00 pull requests•Updated Jun 22, 2026Jun 22, 2026

• qrcp-bounded-coherence-obstruction

  Public
  Lean formalization of a bounded-coherence obstruction for exact QRCP.

  Lean

  •

  Apache License 2.0

  •00 forks•11 star•00 issues•00 pull requests•Updated May 31, 2026May 31, 2026

• LeanSearch-v2

  Public
  Python

  •

  Apache License 2.0

  •33 forks•2121 stars•00 issues•00 pull requests•Updated May 18, 2026May 18, 2026

• TreeSearch

  Public
  Lean

  •

  Apache License 2.0

  •00 forks•33 stars•00 issues•00 pull requests•Updated May 10, 2026May 10, 2026

• shouyi

  Public
  Python

  •

  Apache License 2.0

  •00 forks•77 stars•00 issues•00 pull requests•Updated May 5, 2026May 5, 2026

• Aria-autoformalizer

  Public
  Python

  •

  Apache License 2.0

  •00 forks•55 stars•00 issues•00 pull requests•Updated Apr 15, 2026Apr 15, 2026

• openai_client

  Public
  A clean OpenAI-compatible client for Lean 4

  Lean

  •

  Apache License 2.0

  •00 forks•22 stars•00 issues•00 pull requests•Updated Apr 10, 2026Apr 10, 2026

• requests

  Public
  A requests lib for Lean 4

  Lean

  •

  Apache License 2.0

  •00 forks•44 stars•00 issues•00 pull requests•Updated Apr 10, 2026Apr 10, 2026

• metalib

  Public
  A collection of metaprogramming utilities.

  Lean

  •

  Apache License 2.0

  •11 fork•22 stars•00 issues•00 pull requests•Updated Apr 10, 2026Apr 10, 2026

• Anderson-Conjecture

  Public
  Lean

  •

  Apache License 2.0

  •33 forks•3131 stars•00 issues•00 pull requests•Updated Apr 3, 2026Apr 3, 2026

• Archon-FirstProof-problem6-augmentation

  Public
  Lean

  •

  Apache License 2.0

  •00 forks•22 stars•00 issues•00 pull requests•Updated Mar 7, 2026Mar 7, 2026

• Archon-FirstProof-Results

  Public
  Lean

  •

  Apache License 2.0

  •11 fork•2020 stars•00 issues•00 pull requests•Updated Mar 4, 2026Mar 4, 2026

• DeepSeek-Math-V2

  Public
  Python

  •

  Apache License 2.0

  •152152 forks•00 stars•00 issues•00 pull requests•Updated Feb 25, 2026Feb 25, 2026

• FATE

  Public
  The FATE (Formal Algebra Theorem Evaluation) benchmarks.

  MIT License

  •33 forks•5959 stars•11 issue•00 pull requests•Updated Feb 23, 2026Feb 23, 2026

• FATE-M

  Public
  The FATE-M (Formal Algebra Theorem Evaluation - Medium) benchmark.

  Lean

  •

  MIT License

  •22 forks•33 stars•00 issues•00 pull requests•Updated Feb 23, 2026Feb 23, 2026

• FATE-H

  Public
  The FATE-H (Formal Algebra Theorem Evaluation-Hard) benchmark.

  Lean

  •

  MIT License

  •44 forks•44 stars•11 issue•11 pull request•Updated Feb 23, 2026Feb 23, 2026

• FATE-X

  Public
  The FATE-X (Formal Algebra Theorem Evaluation-Extra Hard) benchmark.

  Lean

  •

  MIT License

  •22 forks•44 stars•11 issue•00 pull requests•Updated Feb 23, 2026Feb 23, 2026

• LeanSearch-PS

  Public
  Python

  •00 forks•00 stars•00 issues•00 pull requests•Updated Jan 30, 2026Jan 30, 2026

• mathlib4

  Public
  The math library of Lean 4

  Lean

  •

  Apache License 2.0

  •1.6k1.6k forks•00 stars•00 issues•00 pull requests•Updated Jan 27, 2026Jan 27, 2026

• jixia_db

  Public
  Parse a Lean repo into structured items, and store them in a PostgreSQL database.

  Python

  •

  Apache License 2.0

  •00 forks•11 star•00 issues•00 pull requests•Updated Jan 24, 2026Jan 24, 2026