[bubblyworld]

Why would you think that's a walk in the park? Have you actually tried formalising stuff in Lean/Coq? I have, and even with a postgraduate maths degree behind me it's hard as hell!

The fact that Kevin and his team are formalising FLT is incredible, but they all have decades of experience with this stuff (!!).

Transformers can do arithmetic (and many other things) just fine, do a bit of searching on arxiv and you'll find papers from 2023 showing that nano-scale transformer models suffice. It really is a data problem, not a fundamental limitation with the technology.

[soloist11]

What is your degree in?

[bubblyworld]

Master's studying representation theorems in nonmonotonic logic, left academia for industry during my PhD. Fun spaced out maths problems. I tried to formalize my thesis in Lean but it is nowhere near as simple as you make it out to be.