Why has Lean taken over the formalization world? Previously some big proofs were done in Coq, HOL, etc.
The Fermat's Last Theorem Project
41–42 of 42 posts
Re: The Fermat's Last Theorem Project
#42Earlier quoted context omitted.
Why post this? This appears to be the writings of a crank.
which part
On p.4 you argue that for integers a, b, c and n:
(a + b − c)^n = (c − a)(c − b)g_1(n)
=> a + b − c = [(c − a)(c − b)g_1(n)]^(1/n)
=> g_1(n) | a + b - c