Proof map
Corpus workbench Start from high-rank theorem receipts, unresolved proof debt, or a semantic lens.
theorems 2,253
source 52%
sorry 116
Start here Hong.EulerKronecker.eulerKroneckerConstant_real number theory · EulerKronecker.Definitions · theorem 266 Hong.SquareFree.count_dyadic_range number theory · SquareFree.Corollary2_3 · theorem 263 Hong.Infrastructure.konig_edge_coloring physics · Infrastructure.EdgeColoring · theorem 262 Hong.Moonshine.j_modular_invariant bounds · Moonshine.JInversion · theorem 262
Open proof debt Infrastructure.TamariLattice 100 theorem receipts · 157 source mapped 10 Moonshine.JInversion 10 theorem receipts · 12 source mapped 10 BallantineMerca.QuadFormBounds 25 theorem receipts · 33 source mapped 9
Highest rank Proof debt Source mapped
Audrey 918 thm · 0 sorry positivity · bounds · optimization Becky 195 thm · 0 sorry positivity · bounds · optimization Eisler 171 thm · 2 sorry positivity · bounds · optimization Hong 487 thm · 107 sorry positivity · bounds · number theory Jill 476 thm · 7 sorry positivity · bounds · physics Robert 6 thm · 0 sorry number theory · streaming stats · real analysis Audrey positivity · bounds · optimization · physics
theorem Audrey.Papers.Shegelski1996.lateCurlCoeff_pos ∀ (S : Audrey.Papers.Shegelski1996.ShegelskiRock), Real.instLT.lt 0 (Audrey.Papers.Shegelski1996.lateCurlCoeff S)theorem Audrey.Papers.Shegelski1996.predictedCurlDistance_pos Real.instLT.lt 0 Audrey.Papers.Shegelski1996.predictedCurlDistancetheorem Audrey.Universality.HertzPair.Estar_pos ∀ (self : Audrey.Universality.HertzPair), Real.instLT.lt 0 self.Estartheorem Audrey.Universality.HertzPair.Rstar_pos ∀ (self : Audrey.Universality.HertzPair), Real.instLT.lt 0 self.Rstartheorem Audrey.Papers.Shegelski2003.κ_2003_pos Real.instLT.lt 0 Audrey.Papers.Shegelski2003.κ_2003
Audrey.GameTree.FullGameState.end_num audrey def Audrey.Rotation.SpinModel.casesOn audrey def Audrey.Onitama.instDecidableEqPhase audrey def Audrey.Strategy.ShotType.ctorElimType audrey def Audrey.Papers.Penner2001.stoppingTime_linear_in_v₀ audrey theorem Audrey.Papers.Nyberg2013.NybergRock.v₀ audrey def Audrey.Strategy.Prob.mk.sizeOf_spec audrey theorem Audrey.GameTree.applyAction.eq_3 audrey theorem Audrey.Sweeping.SweepParams.recOn audrey def Audrey.Papers.Kostuk2001.KWSState.ctorIdx audrey def Audrey.IceField.FrictionField.mk.noConfusion audrey def Audrey.Optimization.Discoveries.ParetoPoint.mk audrey def Audrey.FirstPrinciples.MaenoFromShegelski.maeno_formula_from_shegelski audrey theorem Audrey.Constants.stoneMassMin audrey def Audrey.Stochastics.hitProb_le_one audrey theorem Audrey.Rotation.CurlKinematics.ω0_pos audrey theorem Audrey.Constants.standardSpin_pos audrey theorem Audrey.Strategy.HammerValue.noConfusion audrey def Audrey.Onitama.GameState.noConfusionType audrey def Audrey.Papers.Shegelski2018.hybridForce_monotone_in_alpha audrey theorem Audrey.Sweeping.Delivery.casesOn audrey def Audrey.IceField.PebbleField.casesOn audrey def Audrey.FirstPrinciples.AsymmetricFriction.frontLoadFactor audrey def Audrey.Friction.lateCurlConst audrey def Audrey.Onitama.value.match_1 audrey def Audrey.Collision.totalKineticEnergy audrey def Audrey.Papers.Shegelski1996.ShegelskiRock.mk.sizeOf_spec audrey theorem Audrey.Trajectory.CurlingRock.mass_pos audrey theorem Audrey.Sweeping.μ_decreasing audrey theorem Audrey.Strategy.HammerAdvantage.mk.inj audrey theorem Audrey.Onitama.GameState audrey inductive Audrey.Strategy.CurlingMDP.noConfusionType audrey def Audrey.Papers.Jensen2004.centrifugalRimForceStandard_pos audrey theorem Audrey.Constants.standardDrawVelocity audrey def Audrey.Strategy.HammerValue.mk audrey def Audrey.Stochastics.propagate_smul audrey theorem Audrey.Onitama.PieceKind.master.elim audrey def Audrey.GameTree.Distribution.noConfusion audrey def Audrey.Strategy.TwoPointChance.mk.injEq audrey theorem Audrey.Strategy.TwoPointChance.noConfusionType audrey def Audrey.Pebble.CurlModel.casesOn audrey def Audrey.Strategy.HammerValue audrey inductive Audrey.Papers.Shegelski2018.PivotWeight.mk audrey def Audrey.Sweeping.SweepParams.mk.sizeOf_spec audrey theorem Audrey.Trajectory.takeout_faster_than_draw audrey theorem Audrey.Papers.WCFRules2024.graniteDensityMax audrey def Audrey.Papers.Jensen2004.coriolisMagnitude audrey def Audrey.Papers.Shegelski2018.PivotWeight.casesOn audrey def Audrey.Papers.Penner2001.PennerStone.mk.noConfusion audrey def Audrey.Onitama.PieceKind.student.sizeOf_spec audrey theorem Audrey.GameTree.instDecidableEqFullGameState.decEq.match_1 audrey def Audrey.GameTree.Distribution.mk.inj audrey theorem Audrey.Constants.hammerValue.eq_9 audrey theorem Audrey.Universality.hertz_pressure_distribution audrey theorem Audrey.GameTree.gridSize audrey def Audrey.FirstPrinciples.RotationDecay.rotationalStoppingTime audrey def Audrey.Pebble.HertzSphere.noConfusionType audrey def Audrey.Optimization.ScoredFrontier.ctorIdx audrey def Audrey.Constants.nearHog audrey def Audrey.Papers.Shegelski1996.ShegelskiRock.μ_pos audrey theorem Audrey.Optimization.Turn.ctorIdx audrey def Audrey.Trajectory.FrictionLaw.mu_bound_pos audrey theorem Audrey.Onitama.initialBoard audrey def Audrey.Papers.Nyberg2013.NybergRock.ctorIdx audrey def Audrey.GameTree.Distribution.mk audrey def Audrey.FirstPrinciples.HammerFromBackwardInduction.EndOutcomeDistribution.noConfusion audrey def Audrey.Sweeping.FrictionModel.μ0_pos audrey theorem Audrey.Pebble.contactArea audrey def Audrey.Strategy.CurlingState.score_diff audrey def Audrey.Optimization.feasibleReals_isCompact_perTurn audrey theorem Audrey.Constants.sweepFrictionRatio audrey def Audrey.Papers.Kostuk2001.KWSState.recOn audrey def Audrey.Strategy.kwsHammerValue audrey def Audrey.Papers.Penner2001.lateralTorqueMax audrey def Audrey.Onitama.GameState.mk audrey def Audrey.FirstPrinciples.PebbleDensityOptimum.pebbleDensity_in_optimum_range audrey theorem Audrey.Stochastics.NormalCdf.bounded_above audrey theorem Audrey.Onitama.Cards.all_names_nodup audrey theorem Audrey.Strategy.GameState.noConfusion audrey def Audrey.Onitama.Phase.ofNat_ctorIdx audrey theorem
Select a theorem Select a module region or declaration to inspect its Lean statement, source path, cached proof metadata, and live Kimina REPL verdict.
Module regions encode declaration volume, theorem count, source coverage, and cached sorry debt.