6 ms·
IIUC, a Gemini-based system could translate the natural language questions into Lean, but in the blog post they don’t really commit to whether this was done jus
by clbrmbr 2y ago
IIUC, a Gemini-based system could translate the natural language questions into Lean, but in the blog post they don’t really commit to whether this was done just to generate training data or was used in the competition.
- deleted 2y ago[deleted]
- cygaril 2y agoFormalizations for the competition were done by hand.