Pith. sign in

Chemistry

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

219 modules · 931 thm/lemma · 10780 lines
module thm lemma def lines papers
Chemistry.Acetic_Acid_pKa_RS 4 0 3 36 -
Chemistry.Acetone_Boiling_RS 4 0 3 36 -
Chemistry.AcidBaseEquilibriumFromJCost 4 0 3 47 -
Chemistry.AcidBaseTheoriesFromConfigDim 1 0 1 34 -
Chemistry.AcidCatalysis_FromJCost 4 0 3 37 -
Chemistry.AcidicStrengthFromPhiLadder 4 0 3 37 -
Chemistry.ActivityCoefficient3_FromJCost 4 0 3 36 -
Chemistry.Arrhenius_A_Factor_v3 4 0 3 36 -
Chemistry.AtomicRadii 23 0 5 148 -
Chemistry.Autocatalysis_FromJCost 4 0 3 36 -
Chemistry.Avogadro_RS 4 0 3 36 -
Chemistry.BiochemRS_001 4 0 3 36 -
Chemistry.BiochemRS_002 4 0 3 36 -
Chemistry.BiochemRS_003 4 0 3 36 -
Chemistry.BiochemRS_004 4 0 3 36 -
Chemistry.BiochemRS_005 4 0 3 36 -
Chemistry.BiochemRS_006 4 0 3 36 -
Chemistry.BiochemRS_007 4 0 3 36 -
Chemistry.BiochemRS_008 4 0 3 36 -
Chemistry.BiochemRS_009 4 0 3 36 -
Chemistry.BiochemRS_010 4 0 3 36 -
Chemistry.BiochemRS_011 4 0 3 36 -
Chemistry.BiochemRS_012 4 0 3 36 -
Chemistry.BiochemRS_013 4 0 3 36 -
Chemistry.BiochemRS_014 4 0 3 36 -
Chemistry.BiochemRS_015 4 0 3 36 -
Chemistry.BiochemRS_016 4 0 3 36 -
Chemistry.BiochemRS_018 4 0 3 36 -
Chemistry.BiochemRS_019 4 0 3 36 -
Chemistry.BiochemRS_020 4 0 3 36 -
Chemistry.BioinorganicFromJCost 4 0 3 36 -
Chemistry.Boltzmann_kT_RS 4 0 3 36 -
Chemistry.BondAngles 7 1 7 168 -
Chemistry.Bond_Angle_Water5 4 0 3 36 -
Chemistry.Bond_Dissociation_RS 4 0 3 36 -
Chemistry.BufferCapacityFromJCost 4 0 3 47 -
Chemistry.Carbon_Ionization_RS 4 0 3 36 -
Chemistry.CatalysisActivationEnergy2 4 0 3 37 -
Chemistry.CatalysisChiralFromJCost 4 0 3 37 -
Chemistry.CatalysisElectrochem_FromJCost 4 0 3 37 -
Chemistry.CatalysisKineticsFromJCost 4 0 3 37 -
Chemistry.CatalysisQualityFactorFromJCost 4 0 3 47 -
Chemistry.CatalystSelectivityFromJCost 1 0 1 37 -
Chemistry.ChemicalPotential3_FromJCost 4 0 3 36 -
Chemistry.Chiral3_Induction_FromJCost 4 0 3 36 -
Chemistry.Chromatography3_FromJCost 4 0 3 36 -
Chemistry.Cohesion_Energy3_FromJCost 4 0 3 36 -
Chemistry.ColloidStabilityFromJCost 1 0 1 35 -
Chemistry.ComplexationConstantFromJCost 4 0 3 37 -
Chemistry.Crosslink_Density3_FromJCost 4 0 3 36 -
Chemistry.CrystalGrowthFromPhiLadder 2 0 2 49 -
Chemistry.CrystalStructure 10 0 10 191 -
Chemistry.CrystalSymmetry 14 0 18 241 -
Chemistry.Crystal_Field3_FromJCost 4 0 3 36 -
Chemistry.Dielectric_Water_RS 4 0 3 36 -
Chemistry.Diels_Alder3_FromJCost 4 0 3 36 -
Chemistry.Diels_Alder_RS_v3 4 0 3 36 -
Chemistry.ESR5 4 0 3 36 -
Chemistry.ESSolution5 4 0 3 36 -
Chemistry.ElectrochemicalSeriesFromPhiLadder 3 0 2 54 -
Chemistry.ElectrochemicalWindowFromJCost 4 0 3 47 -
Chemistry.Electrode_Potential_FromPhiLadder 4 0 3 36 -
Chemistry.Electrolysis3_FromJCost 4 0 3 36 -
Chemistry.ElectronAffinity 16 0 5 151 -
Chemistry.Electronegativity 16 0 2 155 -
Chemistry.Electronegativity2_FromJCost 4 0 3 36 -
Chemistry.ElectronegativityFromPhiLadder 4 0 3 51 -
Chemistry.Electronegativity_Phi_RS 4 0 3 36 -
Chemistry.EquilibriumConstantFromJCost 4 0 3 47 -
Chemistry.Ethanol_Boiling_RS 4 0 3 36 -
Chemistry.FPDepression4 4 0 3 36 -
Chemistry.Ferromagnetism 14 0 13 227 -
Chemistry.Flash_Point_FromJCost 4 0 3 36 -
Chemistry.Flory_Parameter3_FromJCost 4 0 3 36 -
Chemistry.Gas_Phase3_Reaction_FromJCost 4 0 3 36 -
Chemistry.GelPoint_FromJCost 4 0 3 36 -
Chemistry.GlassTransition 5 0 8 140 -
Chemistry.GreenChemistryFromJCost 4 0 3 37 -
Chemistry.GreenMetricsTenPrinciples 4 0 3 36 -
Chemistry.HaberBoschFromJCost 1 0 1 41 -
Chemistry.HaberBoschFromPhiLadder 6 0 5 102 -
Chemistry.Hammett4_v2 4 0 3 36 -
Chemistry.Henry_Law3_FromJCost 4 0 3 36 -
Chemistry.Hydrogen_Bonding_Energy_RS 4 0 3 36 -
Chemistry.IR5 4 0 3 36 -
Chemistry.Inorganic3_Crystal_FromJCost 4 0 3 36 -
Chemistry.IonicBond 7 0 12 198 -
Chemistry.IonizationEnergy 4 0 6 130 -
Chemistry.Isothermal_Calorimetry 4 0 3 36 -
Chemistry.Isotope_Effect2_FromJCost 4 0 3 36 -
Chemistry.Kinetic_Resolution3_FromJCost 4 0 3 36 -
Chemistry.LaserLinewidthFromJCost 4 0 3 47 -
Chemistry.LewisAcid4_v2 4 0 3 36 -
Chemistry.LewisAcidFromJCost 4 0 3 37 -
Chemistry.LigandFieldFromPhiLadder 4 0 3 37 -
Chemistry.LipidBilayerThicknessFromPhi 4 0 3 37 -
Chemistry.Liquid_Crystal_Phase_FromJCost 4 0 3 36 -
Chemistry.MaillardReactionThresholdFromJCost 0 0 1 39 -
Chemistry.MaillardTemperatureLadder 4 0 3 80 -
Chemistry.MaillardThresholdFromJCost 3 0 1 46 -
Chemistry.Marcus_Theory_RS_v3 4 0 3 36 -
Chemistry.MetallicBond 6 0 10 177 -
Chemistry.MicelleCMC_FromJCost 4 0 3 37 -
Chemistry.MolecularOrbitalGapFromJCost 4 0 3 43 -
Chemistry.MolecularOrbitals4FromJCost 4 0 3 36 -
Chemistry.MolecularRecognition_FromJCost 4 0 3 36 -
Chemistry.NMRRelaxationFromPhiLadder 4 0 3 47 -
Chemistry.NMRShielding5 4 0 3 36 -
Chemistry.NMR_Coupling_FromPhi 4 0 3 36 -
Chemistry.NMR_T1rhoFromPhiLadder 4 0 3 37 -
Chemistry.Nematic3_Order_Param_FromJCost 4 0 3 36 -
Chemistry.NuclearMagicIsotopesFromRS 1 0 1 35 -
Chemistry.Nucleation3_FromJCost 4 0 3 36 -
Chemistry.NucleophilicSubs3FromJCost 4 0 3 36 -
Chemistry.NucleophilicityFromJCost 4 0 3 36 -
Chemistry.NucleosideStructureFromConfigDim 3 0 2 46 -
Chemistry.OlefinsFromPhiLadder 4 0 3 37 -
Chemistry.OrganicFunctionalGroupsFromConfigDim 1 0 1 33 -
Chemistry.Organocatalysis3_FromJCost 4 0 3 36 -
Chemistry.Osmosis3_FromJCost 4 0 3 36 -
Chemistry.OxidationReductionPotentialFromJCost 4 0 3 47 -
Chemistry.OxidationStateFromConfigDim 5 0 3 77 -
Chemistry.OxidationStatesDerived 8 0 1 77 -
Chemistry.OxidativePhosphoFromJCost 4 0 3 37 -
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.PhaseSeparationFromJCost 4 0 3 47 -
Chemistry.Phase_Transition_CO2From_JCost 4 0 3 37 -
Chemistry.PhotocatalysisEfficiency2FromJCost 4 0 3 36 -
Chemistry.PhotocatalysisFromJCost 4 0 3 37 -
Chemistry.Photodissociation3_FromJCost 4 0 3 36 -
Chemistry.PhotoelectronSpectroscopy 4 0 3 36 -
Chemistry.Photosynthesis2FromJCost 4 0 3 36 -
Chemistry.Photosynthesis3_FromPhiLadder 4 0 3 36 -
Chemistry.Polarimetry3FromJCost 4 0 3 36 -
Chemistry.PolarizabilityFromPhiLadder 4 0 3 47 -
Chemistry.PolarizationCatastropheFromJCost 4 0 3 37 -
Chemistry.PolymerChainLengthFromPhiLadder 2 0 2 45 -
Chemistry.PolymerChainStatisticsFromJCost 4 0 3 37 -
Chemistry.PolymerMorphologyFromConfigDim 1 0 1 36 -
Chemistry.PolymerSolubilityFromJCost 4 0 3 37 -
Chemistry.Polymer_Crystal3_FromJCost 4 0 3 36 -
Chemistry.PolymerizationKineticFromJCost 4 0 3 47 -
Chemistry.PolymorphismFromJCost 4 0 3 37 -
Chemistry.PolyolefinsFromJCost 4 0 3 37 -
Chemistry.PrecipitationNucleationFromJCost 4 0 3 47 -
Chemistry.Quasicrystal 6 0 5 110 -
Chemistry.RNATargetedCompounds 3 0 2 88 -
Chemistry.RS_CHM_Structural_001 4 0 3 36 -
Chemistry.RS_CHM_Structural_002 4 0 3 36 -
Chemistry.RS_CHM_Structural_003 4 0 3 36 -
Chemistry.RS_CHM_Structural_004 4 0 3 36 -
Chemistry.RS_CHM_Structural_005 4 0 3 36 -
Chemistry.RS_CHM_Structural_006 4 0 3 36 -
Chemistry.RS_CHM_Structural_007 4 0 3 36 -
Chemistry.RS_CHM_Structural_008 4 0 3 36 -
Chemistry.RS_CHM_Structural_009 4 0 3 36 -
Chemistry.RS_CHM_Structural_010 4 0 3 36 -
Chemistry.RS_Chem_Module_001 4 0 3 36 -
Chemistry.RS_Chem_Module_002 4 0 3 36 -
Chemistry.RS_Chem_Module_003 4 0 3 36 -
Chemistry.RS_Chem_Module_004 4 0 3 36 -
Chemistry.RS_Chem_Module_005 4 0 3 36 -
Chemistry.RS_Chem_Module_006 4 0 3 36 -
Chemistry.RS_Chem_Module_007 4 0 3 36 -
Chemistry.RS_Chem_Module_008 4 0 3 36 -
Chemistry.RS_Chem_Module_009 4 0 3 36 -
Chemistry.RS_Chem_Module_010 4 0 3 36 -
Chemistry.RS_Chem_Module_011 4 0 3 36 -
Chemistry.RS_Chem_Module_012 4 0 3 36 -
Chemistry.Radical_Chain3_FromJCost 4 0 3 36 -
Chemistry.Radical_Clock3_FromJCost 4 0 3 36 -
Chemistry.Radical_Stability3_FromJCost 4 0 3 36 -
Chemistry.RadioactivePrecursorFromJCost 4 0 3 37 -
Chemistry.RateConstantFromPhiLadder 4 0 3 47 -
Chemistry.ReactionCoordinateFromJCost 4 0 3 51 -
Chemistry.ReactionMechanismFromJCost 4 0 3 37 -
Chemistry.ReactionMechanismsFromConfigDim 1 0 1 35 -
Chemistry.Reaction_Calorimetry3_FromJCost 4 0 3 36 -
Chemistry.Reaction_Network2_FromJCost 4 0 3 36 -
Chemistry.Reaction_Selectivity2 4 0 3 36 -
Chemistry.ReactiveOxygenFromJCost 4 0 3 37 -
Chemistry.ReactiveOxygenSpeciesFromJCost 3 0 1 45 -
Chemistry.Semiconductor_Band_Gap2 4 0 3 36 -
Chemistry.Sodium_Ionization_RS 4 0 3 36 -
Chemistry.SolGelTransitionFromJCost 4 0 3 37 -
Chemistry.SolidElectrolyte3FromJCost 4 0 3 36 -
Chemistry.SolubilityProductFromJCost 4 0 3 51 -
Chemistry.SolubilityRuleFromJCost 4 0 3 47 -
Chemistry.SolvationFreeEnergyFromJCost 4 0 3 43 -
Chemistry.SolvationShellsFromConfigDim 3 0 2 51 -
Chemistry.SolventExtractionFromJCost 4 0 3 37 -
Chemistry.SolventPolarityFromJCost 4 0 3 51 -
Chemistry.SolventViscosityFromPhiLadder 4 0 3 37 -
Chemistry.StereochemistryClassesFromConfigDim 1 0 1 33 -
Chemistry.Structural_Chemistry_mod27 4 0 3 36 -
Chemistry.Structural_Chemistry_mod37 4 0 3 36 -
Chemistry.Structural_Chemistry_mod47 4 0 3 36 -
Chemistry.Structural_Chemistry_mod57 4 0 3 36 -
Chemistry.Structural_Chemistry_mod67 4 0 3 36 -
Chemistry.Structural_Chemistry_mod77 4 0 3 36 -
Chemistry.Structural_Chemistry_mod87 4 0 3 36 -
Chemistry.Structural_Chemistry_mod97 4 0 3 36 -
Chemistry.Sublimation3_FromJCost 4 0 3 36 -
Chemistry.SuperconductingTc 6 0 6 143 -
Chemistry.Surface_Tension2_FromPhiLadder 4 0 3 36 -
Chemistry.TautomerRatio5 4 0 3 36 -
Chemistry.Thermal_Runaway3_FromJCost 4 0 3 36 -
Chemistry.VanDerWaals 9 0 7 320 -
Chemistry.VaporPressureFromPhiLadder 4 0 3 37 -
Chemistry.VdWEquationFromJCost 4 0 3 47 -
Chemistry.Vibrational_Mode2_FromJCost 4 0 3 36 -
Chemistry.Viscosity3_FromPhiLadder 4 0 3 36 -
Chemistry.Water_Density_RS 4 0 3 36 -
Chemistry.Water_pKw_RS 4 0 3 36 -
Chemistry.ZieglerNattaFromJCost 4 0 3 51 -

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