pith. machine review for the scientific record. sign in

Mathematics

Mathematics modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

70 modules · 357 thm/lemma · 6593 lines
module thm lemma def lines papers
Mathematics.AbstractAlgebraFromRS 3 0 3 47
Mathematics.AbstractHarmoniAnalysisFromRS 2 0 2 40
Mathematics.AbstractHarmonicAnalysisFromRS 2 0 2 40
Mathematics.AlgebraicGeometryFromRS 2 0 2 43
Mathematics.AlgebraicStructuresFromConfigDim 1 0 1 36
Mathematics.BirchSwinnertonDyerStructure 2 0 1 28
Mathematics.BirchTateStructure 14 0 4 172
Mathematics.BooleanAlgebraFromRS 3 0 2 49
Mathematics.CalculusVariationsFromRS 3 0 1 48
Mathematics.CategoryTheoryConceptsFromConfigDim 1 0 1 32
Mathematics.CategoryTheoryFromRS 1 0 1 34
Mathematics.CombinatoricsFromRS 4 0 1 51
Mathematics.ComplexAnalysisFromRS 2 0 2 41
Mathematics.ComplexNumbers 15 0 5 283
Mathematics.ComputationalComplexityFromRS 2 0 2 41
Mathematics.ConwayGroupStructuralFromRS 3 0 4 43
Mathematics.CubicSymmetryGroupFromRS 4 0 4 45
Mathematics.DifferentialGeometryFromRS 3 0 3 43
Mathematics.EightFoldWayFromRS 3 0 3 50
Mathematics.ElementaryRegularNumberSystems 1 0 1 35
Mathematics.Euler 12 0 16 283
Mathematics.FibonacciSequenceFromRS 9 0 1 61
Mathematics.FourColorTheoremFromRS 3 0 4 47
Mathematics.FourierAnalysisFromRS 3 0 3 55
Mathematics.FundamentalTheoremCalculusFromRS 3 0 1 49
Mathematics.GameTheoryDepthFromRS 1 0 1 35
Mathematics.GodelTheoremsStructuralFromRS 1 0 1 38
Mathematics.GoldbachFromRS 3 0 1 54
Mathematics.GraphInvariantsFromConfigDim 1 0 1 35
Mathematics.GraphTheoryDepthFromRS 3 0 6 50
Mathematics.GraphTheoryFromRS 5 0 4 47
Mathematics.HodgeAlgebraicCycles 5 0 5 164
Mathematics.HodgeConjEvenDimFromRS 2 0 2 51
Mathematics.HodgeConjecture 9 0 4 281
Mathematics.HodgeConjectureStructure 2 0 1 28
Mathematics.HodgeHardDirection 6 0 0 154
Mathematics.HodgeHarmonicForms 8 0 2 198
Mathematics.ImaginaryUnit 10 0 4 234
Mathematics.InformationTheoryFromRS 3 0 1 48
Mathematics.KnotInvariantsFromRS 1 0 1 35
Mathematics.LanglandsFromRecognitionCost 4 0 4 99
Mathematics.LinearAlgebraFromRS 3 0 3 48
Mathematics.LogicSystemsFromConfigDim 1 0 1 32
Mathematics.MeasureTheoryFromRS 2 0 1 45
Mathematics.NavierStokesRegimes 3 0 2 55
Mathematics.NumberSystemsFromRS 2 0 1 42
Mathematics.NumberTheoryFromRS 5 0 2 69
Mathematics.NumericalAnalysisFromRS 3 0 3 47
Mathematics.OperationsResearchFromRS 2 0 1 39
Mathematics.OptimizationProblemClassesFromConfigDim 1 0 1 32
Mathematics.OptimizationTheoryFromRS 3 0 1 48
Mathematics.P_vs_NP_From_RS 3 0 2 56
Mathematics.PartialDifferentialEquationsFromRS 1 0 1 34
Mathematics.Pi 8 0 9 314
Mathematics.PrimeCostSpectrumFromJCost 2 0 1 43
Mathematics.PrimeGapFromJCost 2 0 1 44
Mathematics.ProbabilityTheoryFromRS 3 0 1 49
Mathematics.RamanujanBridge 0 0 0 69
Mathematics.RamanujanBridge.CongruenceQ3Bridge 45 0 4 389
Mathematics.RamanujanBridge.ContinuedFractionPhi 10 2 5 312
Mathematics.RamanujanBridge.DirectedFlux24 8 0 4 192
Mathematics.RamanujanBridge.MockThetaPhantom 31 0 4 493
Mathematics.RamanujanBridge.PhiLadderStability 16 4 3 284
Mathematics.RamanujanBridge.RamanujanPiFactors 16 0 2 183
Mathematics.RamanujanBridge.ZeckendorfJCost 8 0 3 246
Mathematics.RiemannZetaFromRS 1 0 1 26
Mathematics.SetTheoryFromRS 3 0 2 48
Mathematics.StochasticProcessesFromRS 1 0 1 33
Mathematics.TopologyFromRS 2 0 2 38
Mathematics.ZetaSpecialValuesFromRS 1 0 1 36

full source mirrored from github.com/jonwashburn/shape-of-logic