Checked implications

What the discovery pipeline found and Lean's kernel checked: from the source statements, as hypotheses, a derivation of the target's statement (or, for a composition, of the statement it gives), within a fixed set of rules and depth. Each entry shows the exact statement Lean checked, the steps, the substitutions and the assumptions it discharged. The search never finds every implication, and an implication it did not find may still hold.

Provenance. Recorded: each checked entry was checked by Lean's kernel when the pipeline ran, in the environment named; a site build that shows the catalogue does not run Lean again. Rule set: rules-1:c88d27fdc5e2730d (declarations extracted under rules-1:2417946e30d8228a (solutions, statements)); Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release); Mathlib d13f23b723b8; openai/math at fd4aeeb2ee4f.

100 checked: connection 14, within one challenge file 67, the source restated (same proposition up to definitions) 3, other direction of an equivalence 1, same statement as the source 2, through a structure's field (what its objects carry by definition) 13. 14 are connections; the rest are routine and grouped. 374 proof dependencies were read from elaborated proof terms (a separate record). 3719 attempts established nothing and 4 were rejected: notes.

Loading…