"And then the first sentence of chapter 1 of the paper proper is "Consider quasi-finite separated commutative group schemes of finite presentation over the base \(S:= \mathrm{Spec}(\mathbb{Z}) \) which are finite flat group schemes over \(S':= \mathrm{Spec}(\mathbb{Z}[1/N]) \)". At the time of writing (May 2024), Lean’s algebraic geometry cannot get us through the first sentence of Mazur’s proof, which occupies pages 43 to 172 of the paper (not including the appendix or references, that’s just the proof). Anyone interested in formalising Mazur’s paper should make a formalisation of its first sentence their first milestone."
— @xenaproject

#FermatsLastTheorem

There's a type of #maths problems thatt can be described as "deceptively simple". They sound straightforward when described, but solving them is another matter. #FermatsLastTheorem is one, the #CollatzConjecture is another.

I'm sure that the proof of the latter must have something to do with how the operation 3n+1 affects the binary representation of the number, but I'm not sure where to go next.

This guy opened a YouTube channel 3 years ago uploading videos of a proof of Fermat's Last Theorem, beginning from zero.
Now he is still at the introduction of basic topology.
https://www.youtube.com/@greg55666/videos
#maths #mathematics #fermatslasttheorem