Pith. sign in

Mathematics

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

60 modules · 425 thm/lemma · 9131 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.BipartiteDistanceSpectrum 1 0 11 157 -
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.DistanceShellMultiplicity 235 0 83 5701 -
Mathematics.EightFoldWayFromRS 3 0 3 50 -
Mathematics.ElementaryRegularNumberSystems 1 0 1 35 -
Mathematics.Euler 12 0 16 283 -
Mathematics.Euler_Phi_RS 4 0 3 36 -
Mathematics.FibonacciSequenceFromRS 9 0 1 61 -
Mathematics.Fibonacci_Phi_Limit_RS 4 0 3 36 -
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 63 -
Mathematics.GraphInvariantsFromConfigDim 1 0 1 35 -
Mathematics.GraphTheoryDepthFromRS 3 0 6 50 -
Mathematics.GraphTheoryFromRS 5 0 4 47 -
Mathematics.InformationTheoryFromRS 3 0 1 48 -
Mathematics.KnotInvariantsFromRS 1 0 1 35 -
Mathematics.LinearAlgebraFromRS 3 0 3 48 -
Mathematics.LogicSystemsFromConfigDim 1 0 1 32 -
Mathematics.MeasureTheoryFromRS 2 0 1 45 -
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.PartialDifferentialEquationsFromRS 1 0 1 34 -
Mathematics.Pi 8 0 9 314 -
Mathematics.ProbabilityTheoryFromRS 3 0 1 49 -
Mathematics.ProjectionMultiplicityMethod 1 0 1 114 -
Mathematics.RS_MTH_Structural_001 4 0 3 36 -
Mathematics.RS_MTH_Structural_002 4 0 3 36 -
Mathematics.RS_MTH_Structural_003 4 0 3 36 -
Mathematics.RS_MTH_Structural_004 4 0 3 36 -
Mathematics.RS_MTH_Structural_005 4 0 3 36 -
Mathematics.RS_MTH_Structural_006 4 0 3 36 -
Mathematics.RS_MTH_Structural_007 4 0 3 36 -
Mathematics.RS_MTH_Structural_008 4 0 3 36 -
Mathematics.RS_MTH_Structural_009 4 0 3 36 -
Mathematics.RS_MTH_Structural_010 4 0 3 36 -
Mathematics.SetTheoryFromRS 3 0 2 48 -
Mathematics.StochasticProcessesFromRS 1 0 1 33 -
Mathematics.TopologyFromRS 2 0 2 38 -

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