TauCetiProject

TauCetiProject/TauCeti

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

14 stars 7 forks 14 watchers Lean Apache License 2.0
View on GitHub Website
4 Open Issues Need Help Last updated: Jul 8, 2026

Open Issues Need Help

View All on GitHub
Analysis/Contour: make the on-curve winding-number layer real (HW Prop 2.2 and regularity-condition witnesses) 12 days ago
help wanted roadmap/ContourIntegration
TauCetiProject/TauCeti
14

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Lean
Analysis/Complex/Conformal: prove the Schwarz reflection crossing theorem 30 days ago
help wanted roadmap/ConformalMapping
TauCetiProject/TauCeti
14

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Lean
CompletelyMonotone: final assembly of Bernstein's theorem 30 days ago
help wanted roadmap/OneParameterSemigroups
TauCetiProject/TauCeti
14

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Lean
KnotTheory/Grid: prove the square of the fully blocked grid differential is zero 30 days ago
help wanted roadmap/CombinatorialHeegaardFloer
TauCetiProject/TauCeti
14

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Lean