Unsolved @ Lean 
An auto-updating collection of wanted proofs (sorry and proof_wanted) in the Lean4 theorem prover across established projects.
The raw list of wanted proofs is also available in ND-JSON at ./repositories.json.
There are currently 209 wanted proofs.
Repositories
Wanted Proofs
Mathlib.Geometry.Manifold.PoincareConjecture.lean:39 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:43 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:48 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:61 (playground)Mathlib.Geometry.Manifold.PoincareConjecture.lean:68 (playground)Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic.lean:104 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:223 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:230 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:237 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:244 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:250 (playground)Mathlib.Order.KrullDimension.lean:809 (playground)Mathlib.Order.KrullDimension.lean:812 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:253 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:257 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:380 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:382 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:385 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:390 (playground)Mathlib.RingTheory.KrullDimension.Basic.lean:66 (playground)Mathlib.RingTheory.KrullDimension.Basic.lean:69 (playground)Mathlib.Data.ENat.Lattice.lean:127 (playground)Mathlib.Data.ENat.Lattice.lean:128 (playground)Mathlib.Data.ENat.Lattice.lean:129 (playground)Mathlib.Data.ENat.Lattice.lean:130 (playground)Mathlib.Data.ENat.Lattice.lean:132 (playground)Mathlib.Data.ENat.Lattice.lean:135 (playground)Mathlib.Data.ENat.Lattice.lean:139 (playground)Mathlib.Data.ENat.Lattice.lean:143 (playground)Mathlib.Data.ENat.Lattice.lean:145 (playground)Mathlib.Data.ENat.Lattice.lean:146 (playground)Mathlib.Data.ENat.Lattice.lean:203 (playground)Mathlib.Data.ENat.Lattice.lean:206 (playground)FLT.Basic.Reductions.lean:324FLT.Basic.Reductions.lean:334FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional.lean:24FLT.EllipticCurve.Torsion.lean:35FLT.EllipticCurve.Torsion.lean:39FLT.EllipticCurve.Torsion.lean:44FLT.EllipticCurve.Torsion.lean:49FLT.EllipticCurve.Torsion.lean:55FLT.EllipticCurve.Torsion.lean:61FLT.EllipticCurve.Torsion.lean:64FLT.EllipticCurve.Torsion.lean:69FLT.EllipticCurve.Torsion.lean:73FLT.EllipticCurve.Torsion.lean:77FLT.Mathlib.Topology.Algebra.Module.ModuleTopology.lean:167FLT.Mathlib.Topology.Algebra.Module.ModuleTopology.lean:202FLT.Mathlib.MeasureTheory.Group.Action.lean:26FLT.Mathlib.MeasureTheory.Group.Action.lean:33FLT.Mathlib.MeasureTheory.Group.Action.lean:38FLT.Mathlib.MeasureTheory.Group.Action.lean:43FLT.Mathlib.NumberTheory.Padics.PadicIntegers.lean:62FLT.NumberField.AdeleRing.lean:26FLT.NumberField.AdeleRing.lean:40FLT.NumberField.AdeleRing.lean:114FLT.NumberField.AdeleRing.lean:135FLT.NumberField.AdeleRing.lean:155FLT.NumberField.AdeleRing.lean:161FLT.NumberField.AdeleRing.lean:242FLT.NumberField.InfiniteAdeleRing.lean:28FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:219FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:265FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:285FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:307FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:308FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:368FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:388FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:397FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:405FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:457FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:468FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:473FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:474FLT.AutomorphicRepresentation.Example.lean:307FLT.AutomorphicRepresentation.Example.lean:472FLT.AutomorphicRepresentation.Example.lean:1052FLT.AutomorphicRepresentation.Example.lean:1059FLT.AutomorphicRepresentation.Example.lean:1063FLT.AutomorphicRepresentation.Example.lean:1065FLT.GlobalLanglandsConjectures.GLzero.lean:50FLT.GlobalLanglandsConjectures.GLzero.lean:83FLT.GlobalLanglandsConjectures.GLzero.lean:127FLT.GlobalLanglandsConjectures.GLzero.lean:128FLT.GlobalLanglandsConjectures.GLzero.lean:129FLT.GlobalLanglandsConjectures.GLzero.lean:130FLT.GlobalLanglandsConjectures.GLzero.lean:131FLT.GlobalLanglandsConjectures.GLzero.lean:136FLT.GlobalLanglandsConjectures.GLzero.lean:137FLT.GlobalLanglandsConjectures.GLzero.lean:138FLT.GlobalLanglandsConjectures.GLnDefs.lean:91FLT.GlobalLanglandsConjectures.GLnDefs.lean:94FLT.GlobalLanglandsConjectures.GLnDefs.lean:238FLT.GlobalLanglandsConjectures.GLnDefs.lean:248FLT.DivisionAlgebra.Finiteness.lean:38FLT.DivisionAlgebra.Finiteness.lean:70FLT.HaarMeasure.MeasurableSpacePadics.lean:67banach_tarski.Decomposition.lean:41banach_tarski.Decomposition.lean:44banach_tarski.Decomposition.lean:56banach_tarski.Decomposition.lean:68banach_tarski.Rotations.lean:10banach_tarski.Rotations.lean:15banach_tarski.Rotations.lean:17banach_tarski.Rotations.lean:24banach_tarski.Rotations.lean:44banach_tarski.Rotations.lean:52banach_tarski.Rotations.lean:106banach_tarski.Rotations.lean:107banach_tarski.Rotations.lean:115banach_tarski.Rotations.lean:117banach_tarski.Rotations.lean:122banach_tarski.Rotations.lean:136banach_tarski.Orbit.lean:15banach_tarski.Orbit.lean:27banach_tarski.G_countable.lean:26banach_tarski.G_countable.lean:64banach_tarski.G_countable.lean:65banach_tarski.G_countable.lean:66banach_tarski.Equidecomposable.Def.lean:32banach_tarski.Equidecomposable.Rotations.lean:13banach_tarski.Equidecomposable.Equi_Kreis.lean:18InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:130InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:131InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:135InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:136InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:137InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:161InfinityCosmos.ForMathlib.InfinityCosmos.Isofibrations.lean:70LeanAPAP.FiniteField.lean:137LeanAPAP.FiniteField.lean:166LeanAPAP.FiniteField.lean:183LeanAPAP.FiniteField.lean:193LeanAPAP.FiniteField.lean:216LeanAPAP.FiniteField.lean:223LeanAPAP.Integer.lean:7LeanAPAP.Prereqs.Bohr.Regular.lean:19LeanAPAP.Prereqs.DummyPositivity.lean:18LeanAPAP.Prereqs.DummyPositivity.lean:19LeanAPAP.Prereqs.DummyPositivity.lean:20LeanAPAP.Prereqs.DummyPositivity.lean:22LeanAPAP.Prereqs.DummyPositivity.lean:23LeanAPAP.Prereqs.DummyPositivity.lean:24LeanAPAP.Prereqs.DummyPositivity.lean:25LeanAPAP.Prereqs.DummyPositivity.lean:27LeanAPAP.Prereqs.DummyPositivity.lean:28LeanAPAP.Prereqs.DummyPositivity.lean:29LeanAPAP.Prereqs.DummyPositivity.lean:30LeanAPAP.Prereqs.DummyPositivity.lean:31LeanAPAP.Prereqs.DummyPositivity.lean:32LeanAPAP.Prereqs.DummyPositivity.lean:33LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:54LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:56LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:95LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:139LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:161LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:184LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:186LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:186LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:186LeanAPAP.Prereqs.NewMarcinkiewiczZygmund.lean:187LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:45LeanAPAP.Prereqs.FourierTransform.Convolution.lean:49LeanAPAP.Prereqs.LpNorm.Weighted.lean:107LeanAPAP.Prereqs.LpNorm.Compact.lean:216LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:24LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:42LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:45LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:46LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:54LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:59LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup.lean:60LeanCamCombi.PlainCombi.LittlewoodOfford.lean:33LeanCamCombi.PlainCombi.VanDenBergKesten.lean:97LeanCamCombi.GraphTheory.ExampleSheet1.lean:38LeanCamCombi.GraphTheory.ExampleSheet1.lean:57LeanCamCombi.GraphTheory.ExampleSheet1.lean:70LeanCamCombi.GraphTheory.ExampleSheet1.lean:83LeanCamCombi.GraphTheory.ExampleSheet1.lean:101LeanCamCombi.GraphTheory.ExampleSheet1.lean:113LeanCamCombi.GraphTheory.ExampleSheet1.lean:128LeanCamCombi.GraphTheory.ExampleSheet1.lean:145LeanCamCombi.GraphTheory.ExampleSheet1.lean:164LeanCamCombi.GraphTheory.ExampleSheet1.lean:185LeanCamCombi.GraphTheory.ExampleSheet1.lean:201LeanCamCombi.GraphTheory.ExampleSheet1.lean:218LeanCamCombi.GraphTheory.ExampleSheet1.lean:223LeanCamCombi.GraphTheory.ExampleSheet1.lean:228LeanCamCombi.GraphTheory.ExampleSheet1.lean:251LeanCamCombi.GraphTheory.ExampleSheet1.lean:256LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:117LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:118LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:126LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:127LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:128LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:129LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:130LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:131LeanCamCombi.ExtrProbCombi.BernoulliSeq.lean:132LeanCamCombi.ExtrProbCombi.BinomialRandomGraph.lean:48LeanCamCombi.ExtrProbCombi.BinomialRandomGraph.lean:80LeanCamCombi.ExtrProbCombi.BollobasContainment.lean:31LeanCamCombi.ExtrProbCombi.BollobasContainment.lean:37LeanCamCombi.ExtrProbCombi.Containment.lean:225LeanCamCombi.GrowthInGroups.Lecture4.lean:25LeanCamCombi.GrowthInGroups.Lecture4.lean:30LeanCamCombi.GrowthInGroups.Lecture4.lean:41LeanCamCombi.StableCombi.Rel.lean:38LeanCamCombi.StableCombi.Rel.lean:41