Regarding that claimed breakthrough about AI winning the International Mathematical Olympiad: a reminder that a proof which hangs together logically is not necessarily a proof that makes sense.
Those formalized proofs are so incredibly ugly, it's amazing. Of course it doesn't much of a sensible indentation, but then there are single proof steps where I have no idea what it's even doing. [...] And then there are nonsense mathematical steps. The solution of problem 2 starts with induction, before introducing any variables. It applies induction to the number 12. And it write 12 as
(10)+2
. Then it proceeds to do the whole proof in the base case of the induction, and notices that the induction step is trivial, since the goal is the same as the induction hypothesis (but instead of theassumption
tactic it usescongr 26
).
"The long-term goal is to reinvent the Internet of 25 years ago, but worse."