openai/math

Generated by a source-level scanner, plus a Lean run where it succeeded: see the Trust page. Trust is UNKNOWN wherever Lean did not run. Indented declarations and macro-generated declarations are not listed.

Lean files

122875

Declarations

3572375

Contain sorry

539

Axioms

1

Lean4 Domain Explanation Language (L4DEL): 1393 annotated, 0 flagged (errors or placeholders), 3564870 without an L4DEL annotation. Run lean4-explainer annotate --file <path> for templates. Lean run with Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release) (cache-only rendering).

3572375 declarations, 539 contain sorry, 1 declared as axioms; 122875 files