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 392 wanted proofs.
Repositories
Wanted Proofs
Mathlib.RingTheory.KrullDimension.Basic.lean:85 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:263 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:267 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:404 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:406 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:409 (playground)Mathlib.RingTheory.SimpleModule.Basic.lean:414 (playground)Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic.lean:102 (playground)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.Combinatorics.SimpleGraph.StronglyRegular.lean:67 (playground)Mathlib.Data.EReal.Operations.lean:344 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:226 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:233 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:240 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:247 (playground)Mathlib.CategoryTheory.Limits.Shapes.Countable.lean:253 (playground)Mathlib.Order.KrullDimension.lean:896 (playground)Mathlib.Order.KrullDimension.lean:899 (playground)Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic.lean:116 (playground)Mathlib.Computability.TMComputable.lean:310 (playground)FLT.DivisionAlgebra.Finiteness.lean:56FLT.DivisionAlgebra.Finiteness.lean:72FLT.DivisionAlgebra.Finiteness.lean:129FLT.DivisionAlgebra.Finiteness.lean:132FLT.DivisionAlgebra.Finiteness.lean:176FLT.DivisionAlgebra.Finiteness.lean:205FLT.DivisionAlgebra.Finiteness.lean:217FLT.Basic.Reductions.lean:327FLT.Basic.Reductions.lean:337FLT.AutomorphicRepresentation.Example.lean:212FLT.AutomorphicRepresentation.Example.lean:317FLT.AutomorphicRepresentation.Example.lean:486FLT.AutomorphicRepresentation.Example.lean:1075FLT.AutomorphicRepresentation.Example.lean:1082FLT.AutomorphicRepresentation.Example.lean:1086FLT.AutomorphicRepresentation.Example.lean:1088FLT.GlobalLanglandsConjectures.GLnDefs.lean:180FLT.GlobalLanglandsConjectures.GLnDefs.lean:190FLT.GlobalLanglandsConjectures.GLzero.lean:48FLT.GlobalLanglandsConjectures.GLzero.lean:82FLT.GlobalLanglandsConjectures.GLzero.lean:126FLT.GlobalLanglandsConjectures.GLzero.lean:127FLT.GlobalLanglandsConjectures.GLzero.lean:128FLT.GlobalLanglandsConjectures.GLzero.lean:129FLT.GlobalLanglandsConjectures.GLzero.lean:130FLT.GlobalLanglandsConjectures.GLzero.lean:135FLT.GlobalLanglandsConjectures.GLzero.lean:136FLT.GlobalLanglandsConjectures.GLzero.lean:137FLT.Deformations.Representable.lean:18FLT.QuaternionAlgebra.NumberField.lean:61FLT.QuaternionAlgebra.NumberField.lean:65FLT.QuaternionAlgebra.NumberField.lean:155FLT.QuaternionAlgebra.NumberField.lean:159FLT.QuaternionAlgebra.NumberField.lean:199FLT.QuaternionAlgebra.NumberField.lean:202FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:96FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:104FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:116FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:122FLT.DedekindDomain.FiniteAdeleRing.BaseChange.lean:123FLT.AutomorphicForm.QuaternionAlgebra.Defs.lean:78FLT.AutomorphicForm.QuaternionAlgebra.Defs.lean:188FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional.lean:29FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete.lean:113FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete.lean:118FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete.lean:172FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete.lean:229FLT.HaarMeasure.MeasurableSpacePadics.lean:66FLT.HaarMeasure.HaarChar.AddEquiv.lean:399FLT.HaarMeasure.HaarChar.AddEquiv.lean:474FLT.HaarMeasure.HaarChar.FiniteDimensional.lean:26FLT.HaarMeasure.HaarChar.AdeleRing.lean:89FLT.HaarMeasure.HaarChar.AdeleRing.lean:90FLT.HaarMeasure.HaarChar.AdeleRing.lean:107FLT.HaarMeasure.HaarChar.AdeleRing.lean:111FLT.HaarMeasure.HaarChar.AdeleRing.lean:121FLT.HaarMeasure.HaarChar.AdeleRing.lean:125FLT.HaarMeasure.HaarChar.AdeleRing.lean:138FLT.HaarMeasure.HaarChar.AdeleRing.lean:139FLT.HaarMeasure.HaarChar.AdeleRing.lean:147FLT.HaarMeasure.HaarChar.AdeleRing.lean:158FLT.HaarMeasure.HaarChar.AdeleRing.lean:171FLT.Mathlib.LinearAlgebra.Determinant.lean:48FLT.EllipticCurve.Torsion.lean:37FLT.EllipticCurve.Torsion.lean:41FLT.EllipticCurve.Torsion.lean:46FLT.EllipticCurve.Torsion.lean:50FLT.EllipticCurve.Torsion.lean:56FLT.EllipticCurve.Torsion.lean:62FLT.EllipticCurve.Torsion.lean:65FLT.EllipticCurve.Torsion.lean:70FLT.EllipticCurve.Torsion.lean:74FLT.EllipticCurve.Torsion.lean:78FLT.NumberField.AdeleRing.lean:392Seymour.Matroid.Operations.Sum3.lean:1869Seymour.Matroid.Operations.Sum3.lean:1875Seymour.Matroid.Operations.Sum3.lean:1901Seymour.Matroid.Operations.Sum3.lean:1904Seymour.Matroid.Operations.Sum3.lean:1917Seymour.Matroid.Operations.Sum3.lean:1924Seymour.EasyDirection.lean:24Seymour.HardDirection.lean:8InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Horn.lean:39InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Horn.lean:99InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Horn.lean:155InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:128InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:129InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:133InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:134InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:135InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy.lean:159InfinityCosmos.ForMathlib.InfinityCosmos.Goals.lean:66InfinityCosmos.ForMathlib.InfinityCosmos.Goals.lean:100InfinityCosmos.ForMathlib.InfinityCosmos.Isofibrations.lean:70LeanAPAP.FiniteField.lean:143LeanAPAP.FiniteField.lean:172LeanAPAP.FiniteField.lean:190LeanAPAP.FiniteField.lean:200LeanAPAP.FiniteField.lean:223LeanAPAP.FiniteField.lean:231LeanAPAP.Integer.lean:7LeanAPAP.Prereqs.Bohr.Regular.lean:19LeanAPAP.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.FourierTransform.Convolution.lean:47LeanAPAP.Prereqs.LpNorm.Compact.lean:216LeanAPAP.Prereqs.LpNorm.Weighted.lean:107LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:50LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:94LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:96LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:98LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:100LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:101LeanAPAP.Prereqs.Inner.Hoelder.Compact.lean:131LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:43LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:73LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:75LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:77LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:79LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:80LeanAPAP.Prereqs.Inner.Hoelder.Discrete.lean:111LeanAPAP.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.Mathlib.Topology.Algebra.PontryaginDual.lean:7LeanCamCombi.ExtrProbCombi.BollobasContainment.lean:31LeanCamCombi.ExtrProbCombi.BollobasContainment.lean:37LeanCamCombi.ExtrProbCombi.BinomialRandomGraph.lean:46LeanCamCombi.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.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:160LeanCamCombi.GraphTheory.ExampleSheet1.lean:181LeanCamCombi.GraphTheory.ExampleSheet1.lean:197LeanCamCombi.GraphTheory.ExampleSheet1.lean:214LeanCamCombi.GraphTheory.ExampleSheet1.lean:219LeanCamCombi.GraphTheory.ExampleSheet1.lean:224LeanCamCombi.GraphTheory.ExampleSheet1.lean:247LeanCamCombi.GraphTheory.ExampleSheet1.lean:252LeanCamCombi.PlainCombi.LittlewoodOfford.lean:33LeanCamCombi.PlainCombi.VanDenBergKesten.lean:97LeanCamCombi.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.StableCombi.Rel.lean:38LeanCamCombi.StableCombi.Rel.lean:41LeanCamCombi.GrowthInGroups.Lecture4.lean:25LeanCamCombi.GrowthInGroups.Lecture4.lean:30LeanCamCombi.GrowthInGroups.Lecture4.lean:41Carleson.Classical.ClassicalCarleson.lean:216Carleson.Classical.HilbertStrongType.lean:113Carleson.Classical.HilbertStrongType.lean:123Carleson.Classical.HilbertStrongType.lean:189Carleson.Classical.HilbertStrongType.lean:282Carleson.Classical.HilbertStrongType.lean:286Carleson.Classical.HilbertStrongType.lean:296Carleson.Classical.HilbertStrongType.lean:306Carleson.Classical.HilbertStrongType.lean:319Carleson.Antichain.Basic.lean:313Carleson.Antichain.Basic.lean:330Carleson.Antichain.Basic.lean:335Carleson.Antichain.Basic.lean:383Carleson.Antichain.Basic.lean:389Carleson.Antichain.Basic.lean:414Carleson.Antichain.Basic.lean:424Carleson.Antichain.Basic.lean:432Carleson.Antichain.Basic.lean:455Carleson.Antichain.AntichainTileCount.lean:442Carleson.MetricCarleson.Main.lean:22Carleson.MetricCarleson.Truncation.lean:400Carleson.MetricCarleson.Basic.lean:55Carleson.MetricCarleson.Basic.lean:59Carleson.MetricCarleson.Basic.lean:63Carleson.MetricCarleson.Basic.lean:67Carleson.MetricCarleson.Basic.lean:77Carleson.MetricCarleson.Linearized.lean:30Carleson.ToMathlib.WeakType.lean:847Carleson.ToMathlib.RealInterpolation.Main.lean:332Carleson.ToMathlib.RealInterpolation.Main.lean:382Carleson.ToMathlib.RealInterpolation.Main.lean:383Carleson.ToMathlib.RealInterpolation.Main.lean:386Carleson.ToMathlib.RealInterpolation.Main.lean:391Carleson.ToMathlib.RealInterpolation.Main.lean:399Carleson.ToMathlib.RealInterpolation.Main.lean:414Carleson.ToMathlib.RealInterpolation.Main.lean:964Carleson.ToMathlib.RealInterpolation.Main.lean:1069Carleson.ToMathlib.RealInterpolation.Main.lean:1096Carleson.ToMathlib.RealInterpolation.Main.lean:1158Carleson.ToMathlib.RealInterpolation.Main.lean:1211Carleson.ToMathlib.RealInterpolation.Main.lean:1295Carleson.ToMathlib.RealInterpolation.Main.lean:1393Carleson.ToMathlib.RealInterpolation.Minkowski.lean:430Carleson.ToMathlib.RealInterpolation.Minkowski.lean:432Carleson.ToMathlib.RealInterpolation.Minkowski.lean:451Carleson.ToMathlib.RealInterpolation.Minkowski.lean:554Carleson.ToMathlib.RealInterpolation.Minkowski.lean:770Carleson.ToMathlib.RealInterpolation.Misc.lean:1110Carleson.ToMathlib.RealInterpolation.Misc.lean:1171Carleson.ToMathlib.RealInterpolation.Misc.lean:1242Carleson.ToMathlib.RealInterpolation.Misc.lean:1267Carleson.ToMathlib.RealInterpolation.Misc.lean:1275Carleson.ToMathlib.RealInterpolation.Misc.lean:1276Carleson.ToMathlib.RealInterpolation.Misc.lean:1284Carleson.ToMathlib.Lorentz.lean:153Carleson.ToMathlib.Lorentz.lean:162Carleson.ToMathlib.Lorentz.lean:206Carleson.ToMathlib.Lorentz.lean:210Carleson.ToMathlib.Lorentz.lean:213Carleson.ToMathlib.Lorentz.lean:215Carleson.ToMathlib.Lorentz.lean:216Carleson.ToMathlib.Lorentz.lean:217Carleson.ToMathlib.Lorentz.lean:230Carleson.ToMathlib.Lorentz.lean:230Carleson.ToMathlib.Lorentz.lean:233Carleson.ToMathlib.Lorentz.lean:235Carleson.ToMathlib.Lorentz.lean:236Carleson.ToMathlib.Lorentz.lean:237Carleson.ToMathlib.Lorentz.lean:250Carleson.ToMathlib.Lorentz.lean:256Carleson.ToMathlib.Lorentz.lean:257Carleson.ForestOperator.Forests.lean:368Carleson.ForestOperator.Forests.lean:375Carleson.TwoSidedCarleson.MainTheorem.lean:34Carleson.TwoSidedCarleson.MainTheorem.lean:40Carleson.TwoSidedCarleson.MainTheorem.lean:52Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:1068Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:1078Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:1089Carleson.TwoSidedCarleson.WeakCalderonZygmund.lean:1105Carleson.TwoSidedCarleson.NontangentialOperator.lean:883Carleson.TwoSidedCarleson.NontangentialOperator.lean:957PFR.BoundingMutual.lean:36PFR.TorsionEndgame.lean:50PFR.TorsionEndgame.lean:52PFR.TorsionEndgame.lean:54PFR.TorsionEndgame.lean:58PFR.TorsionEndgame.lean:61PFR.TorsionEndgame.lean:64PFR.TorsionEndgame.lean:67PFR.TorsionEndgame.lean:79PFR.TorsionEndgame.lean:82PFR.TorsionEndgame.lean:89PFR.TorsionEndgame.lean:102PFR.ApproxHomPFR.lean:181PFR.ApproxHomPFR.lean:183PFR.ApproxHomPFR.lean:185PFR.ApproxHomPFR.lean:189PFR.MultiTauFunctional.lean:54PFR.MultiTauFunctional.lean:57PFR.MoreRuzsaDist.lean:527PFR.MoreRuzsaDist.lean:760FormalBook.Chapter_04.lean:48FormalBook.Chapter_04.lean:53FormalBook.Chapter_04.lean:85FormalBook.Chapter_04.lean:182FormalBook.Chapter_04.lean:235FormalBook.Chapter_04.lean:244FormalBook.Chapter_04.lean:283FormalBook.Chapter_05.lean:52FormalBook.Chapter_05.lean:53FormalBook.Chapter_05.lean:58FormalBook.Chapter_05.lean:62FormalBook.Chapter_05.lean:75FormalBook.Chapter_05.lean:78FormalBook.Chapter_05.lean:83FormalBook.Chapter_05.lean:97FormalBook.Chapter_05.lean:103FormalBook.Chapter_05.lean:112FormalBook.Chapter_05.lean:117FormalBook.Chapter_03.lean:37FormalBook.Chapter_03.lean:97FormalBook.Chapter_03.lean:150FormalBook.Chapter_03.lean:154FormalBook.Chapter_03.lean:157FormalBook.Chapter_03.lean:159FormalBook.Chapter_03.lean:174FormalBook.Chapter_21.lean:30FormalBook.Chapter_20.lean:97FormalBook.Chapter_20.lean:109FormalBook.Chapter_20.lean:120FormalBook.Chapter_01.lean:184FormalBook.Chapter_01.lean:185FormalBook.Chapter_01.lean:186FormalBook.Chapter_01.lean:187FormalBook.Chapter_01.lean:188FormalBook.Chapter_01.lean:189FormalBook.Chapter_01.lean:190FormalBook.Chapter_01.lean:339FormalBook.Chapter_01.lean:360FormalBook.Chapter_07.lean:32FormalBook.Chapter_07.lean:38FormalBook.Chapter_02.lean:218FormalBook.Chapter_02.lean:223FormalBook.Chapter_02.lean:227FormalBook.Chapter_06.lean:69FormalBook.Chapter_06.lean:70FormalBook.Chapter_06.lean:76FormalBook.Chapter_06.lean:77FormalBook.Chapter_06.lean:78FormalBook.Chapter_06.lean:79FormalBook.Chapter_06.lean:83FormalBook.Chapter_06.lean:210FormalBook.Chapter_06.lean:238FormalBook.Chapter_06.lean:242FormalBook.Chapter_06.lean:246FormalBook.Chapter_06.lean:255FormalBook.Chapter_06.lean:256FormalBook.Chapter_06.lean:291FormalBook.Chapter_45.lean:41FormalBook.Chapter_45.lean:58FormalBook.Chapter_08.lean:49FormalBook.Chapter_08.lean:58FormalBook.Chapter_08.lean:66FormalBook.Chapter_08.lean:69FormalBook.Chapter_08.lean:77FormalBook.Chapter_08.lean:80FormalBook.Chapter_08.lean:98FormalBook.Chapter_08.lean:110FormalBook.Chapter_08.lean:118FormalBook.Chapter_08.lean:119FormalBook.Chapter_08.lean:124FormalBook.Chapter_08.lean:127FormalBook.Chapter_24.lean:38FormalBook.Chapter_09.lean:27FormalBook.Chapter_09.lean:31FormalBook.Chapter_09.lean:35FormalBook.Chapter_09.lean:39FormalBook.Chapter_44.lean:47FormalBook.Chapter_44.lean:53FormalBook.Chapter_44.lean:106FormalBook.Chapter_44.lean:108