7 ms·
LeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.
by maxwells-daemon 2y ago
LeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.