pith. machine review for the scientific record. sign in

Chemistry

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

42 modules · 222 thm/lemma · 4305 lines
module thm lemma def lines papers
Chemistry.AcidBaseTheoriesFromConfigDim 1 0 1 34
Chemistry.ActivationEnergy 10 0 12 182
Chemistry.AtomicRadii 23 0 5 148
Chemistry.BondAngles 7 1 7 168
Chemistry.CatalysisFromJCost 1 0 1 37
Chemistry.CatalystSelectivityFromJCost 1 0 1 37
Chemistry.ColloidStabilityFromJCost 1 0 1 35
Chemistry.CrystalGrowthFromPhiLadder 2 0 2 49
Chemistry.CrystalStructure 10 0 10 191
Chemistry.CrystalSymmetry 14 0 18 241
Chemistry.ElectrochemicalSeriesFromPhiLadder 3 0 2 54
Chemistry.ElectronAffinity 16 0 5 151
Chemistry.Electronegativity 16 0 2 155
Chemistry.EnvPressure 0 0 3 32
Chemistry.EnzymeCatalysis 8 0 7 201
Chemistry.EnzymeCatalysisThresholdFromJCost 3 0 2 52
Chemistry.Ferromagnetism 14 0 13 227
Chemistry.GlassTransition 5 0 8 140
Chemistry.HaberBoschFromJCost 1 0 1 41
Chemistry.HaberBoschFromPhiLadder 6 0 5 102
Chemistry.IonicBond 7 0 12 198
Chemistry.IonizationEnergy 4 0 6 130
Chemistry.MaillardReactionThresholdFromJCost 0 0 1 39
Chemistry.MaillardTemperatureLadder 4 0 3 80
Chemistry.MaillardThresholdFromJCost 3 0 1 46
Chemistry.MetallicBond 6 0 10 177
Chemistry.NuclearMagicIsotopesFromRS 1 0 1 35
Chemistry.OrganicFunctionalGroupsFromConfigDim 1 0 1 33
Chemistry.PeriodicBlocks 1 0 2 27
Chemistry.PeriodicTable 13 0 23 308
Chemistry.PeriodicTableFromPhiLadder 5 0 2 58
Chemistry.PhaseCoexistenceFromJCost 1 0 1 36
Chemistry.PhaseDiagramTripleFromJCost 1 0 1 43
Chemistry.PolymerChainLengthFromPhiLadder 2 0 2 45
Chemistry.PolymerMorphologyFromConfigDim 1 0 1 36
Chemistry.Quasicrystal 6 0 5 110
Chemistry.ReactionMechanismsFromConfigDim 1 0 1 35
Chemistry.ReactiveOxygenSpeciesFromJCost 3 0 1 45
Chemistry.SolvationShellsFromConfigDim 3 0 2 51
Chemistry.StereochemistryClassesFromConfigDim 1 0 1 33
Chemistry.SuperconductingTc 6 0 6 143
Chemistry.VanDerWaals 9 0 7 320

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