2 ms·
Second author here. Happy to answer any questions about the work!
by maxwells-daemon 2y ago
Second author here. Happy to answer any questions about the work!
- gnahtb 2y agothe infographic in the deepmind blog showed the team built a formalizer network. i wonder how you guys build it. last time i tried chatgpt to translate a math problem into lean it sucks
- maxwells-daemon 2y agoLeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.