Each map below is built from a formal development of several thousand declarations. A handful of techniques propose which statements carry the argument; a Datalog view chooses among them and computes how the chosen statements depend on one another. Every statement carries a one-sentence description, so no knowledge of Lean or Coq is needed.
Double-click a link between two statements to open everything that lies between them.