Pull requests · facebookresearch/atlas-lean

Port composition operators on ℓ² with bounded fibers from IntroductionToFunctionalAnalysis (v1)

#565akiezun opened

Oct 29, 2026

Contributor

Port Banach–Nečas–Babuška theorem for Hilbert spaces from IntroductionToFunctionalAnalysis (v1)

#563akiezun opened

Oct 29, 2026

Contributor

Prove FLM Monster milestones T1–T3 and T5

#526junekim623 opened

Oct 28, 2026

Formalize all FLM milestone construction definitions

#525junekim623 opened

Oct 28, 2026

Add Autoform roadmap for FLM Monster finite-group construction

#524junekim623 opened

Oct 28, 2026

Introducing Atlas/publications as well as a demo paper.

#509abarei96 opened

Oct 28, 2026

14 tasks

1

Port dual of ℓ^p spaces from IntroductionToFunctionalAnalysis (v1)

#465akiezun opened

Oct 27, 2026

Contributor

Port Theorem 6.10 (relative norm, separable form) from NumberTheoryI (v1)

#455akiezun opened

Oct 27, 2026

Contributor

Port monotone simple-function approximation from IntroductionToFunctionalAnalysis (v1)

#438akiezun opened

Oct 27, 2026

Contributor

Add FDSA chapter 13 and 15 quadtree and leftist heap tasks to CSLibExt

#409zhihan opened

Oct 26, 2026

12 tasks done

5

Formalize Eppstein k-shortest-paths (6 lemmas + 2 theorems)

#408losvald opened

Oct 26, 2026

9 of 14 tasks

2

Prove the argument principle for closed piecewise C¹ curves

#406Deicyde opened

Oct 25, 2026

Contributor

Prove the residue theorem for closed piecewise C¹ curves

#405Deicyde opened

Oct 25, 2026

Contributor

Prove the homology form of Cauchy's theorem and integral formula

#404Deicyde opened

Oct 25, 2026

Contributor

Prove harmonic functions on simply connected domains are real parts of holomorphic functions

#403Deicyde opened

Oct 25, 2026

Contributor

Prove Mittag-Leffler's theorem with polynomial corrections

#402Deicyde opened

Oct 24, 2026

Contributor

Prove Taylor's theorem with the Cauchy integral remainder

#401Deicyde opened

Oct 24, 2026

Contributor

Define the residue as a radius-free limit of circle integrals

#400Deicyde opened

Oct 24, 2026

Contributor

Prove Rouché's theorem for simple closed curves

#399Deicyde opened

Oct 24, 2026

Contributor

Classify parabolic, strictly hyperbolic and elliptic Möbius maps by trace

#398Deicyde opened

Oct 24, 2026

Contributor

Prove disjoint circles are Möbius-equivalent to concentric circles

#397Deicyde opened

Oct 24, 2026

Contributor

Prove that circle integrals of functions of z² vanish

#360Deicyde opened

Oct 24, 2026

Contributor

Prove Log(z₁z₂) = Log z₁ + Log z₂ + 2πin with n ∈ {-1, 0, 1}

#359Deicyde opened

Oct 24, 2026

Contributor

2

Prove change of variables for contour integrals

#356Deicyde opened

Oct 24, 2026

Contributor

Prove continuity, holomorphy and symmetry of the divided difference

#353Deicyde opened

Oct 24, 2026

Contributor

Navigation Menu

Repository navigation

All pull requests

Port composition operators on ℓ² with bounded fibers from IntroductionToFunctionalAnalysis (v1)

Port Banach–Nečas–Babuška theorem for Hilbert spaces from IntroductionToFunctionalAnalysis (v1)

Prove FLM Monster milestones T1–T3 and T5

Formalize all FLM milestone construction definitions

Add Autoform roadmap for FLM Monster finite-group construction

Introducing Atlas/publications as well as a demo paper.

Port dual of ℓ^p spaces from IntroductionToFunctionalAnalysis (v1)

Port Theorem 6.10 (relative norm, separable form) from NumberTheoryI (v1)

Port monotone simple-function approximation from IntroductionToFunctionalAnalysis (v1)

Add FDSA chapter 13 and 15 quadtree and leftist heap tasks to CSLibExt

Formalize Eppstein k-shortest-paths (6 lemmas + 2 theorems)

Prove the argument principle for closed piecewise C¹ curves

Prove the residue theorem for closed piecewise C¹ curves

Prove the homology form of Cauchy's theorem and integral formula

Prove harmonic functions on simply connected domains are real parts of holomorphic functions

Prove Mittag-Leffler's theorem with polynomial corrections

Prove Taylor's theorem with the Cauchy integral remainder

Define the residue as a radius-free limit of circle integrals

Prove Rouché's theorem for simple closed curves

Classify parabolic, strictly hyperbolic and elliptic Möbius maps by trace

Prove disjoint circles are Möbius-equivalent to concentric circles

Prove that circle integrals of functions of z² vanish

Prove Log(z₁z₂) = Log z₁ + Log z₂ + 2πin with n ∈ {-1, 0, 1}

Prove change of variables for contour integrals

Prove continuity, holomorphy and symmetry of the divided difference