What does "mathematical output of the AI" even mean? A proof? Intermediate tokens?
It's a Lean program that proves the theorem.
It's a Lean program that proves the theorem.