`fourColorCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.FourColorTheoremFromRS
domain: Mathematics
line: 41 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.FourColorTheoremFromRS on GitHub at line 41.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  38  four_eq_2sq : fourColors = 2 ^ 2
  39  f2sq : fourColors = f2sq_card
  40
  41def fourColorCert : FourColorCert where
  42  four_eq_Dp1 := fourColors_eq_DplusOne
  43  four_eq_2sq := fourColors_eq_2sq
  44  f2sq := four_eq_F2sq
  45
  46end IndisputableMonolith.Mathematics.FourColorTheoremFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.