The Fermat's Last Theorem Project #74
Replies: 11 comments 8 replies
-
This is extremely cool, good luck with the project! |
Beta Was this translation helpful? Give feedback.
-
385 (1637-2022) years later, Fermat's proof of his last theorem has finally been see "https://www.mdpi.com/2227-7390/10/23/4471", that is " On the Nature of Some Euler’s Double Equations Equivalent to Fermat’s Last Theorem" |
Beta Was this translation helpful? Give feedback.
-
sounds really cool |
Beta Was this translation helpful? Give feedback.
-
Thanks for the positive comments! Andrea -- I'll believe your low-level approach if and only if you can formalise it in Lean. I have been sent many many low-level approaches in my life and none of them stand up to the kind of scrutiny which Lean gives. Until then, I think I'll stick with my belief that the only way known to humanity to prove FLT is via elliptic curves and modular forms. |
Beta Was this translation helpful? Give feedback.
-
Dear Mario Carneiro,
I'm sorry, but I don't agree. You evidently know little about the
techniques of classical Diophantine analysis.
I am sending you as an attachment the certainty that my proof is correct.
In my paper, have you seen who the Academic Editor is who authorized the
publication?
Sincerely
Andrea Ossicini
Il giorno ven 3 mag 2024 alle ore 21:14 Mario Carneiro <
***@***.***> ha scritto:
… Hi Andrea,
Against my better judgment I attempted to understand both proofs, and I
believe I found the flaw. Theorem 3 of the paper says: "Fermat’s Last
Theorem is true if and only if a solution is not possible in integers of
Equation (8) with the Q non-zero integer", where equation (8) is equivalent
to $$X_1^nV^2+Y_1^2T^2=Z_1^2P^2$$, $$V^2-T^2=Z_1^2Q^2$$ (which is 2.10 in
the second paper). The proof of this theorem is not given in the first
paper as far as I can tell (it is stated in section 4 with a promised proof
in section 6 but there is no proof in this section but rather a bunch of
unrelated algebraic manipulations followed by an apparent application of
the theorem in the last sentence - "The double equations of Euler are
discordant forms and so the F.L.T. turns out to be true"). There is
something close to a proof of it in the second paper, but the proof
actually shows the opposite: if the FLT is false then this diophantine
system has no solutions with V=T=P and Q nonzero.
Essentially, I believe that equation (8) has no solutions regardless of
the truth of FLT, and so a proof that (8) has no solutions does nothing to
show FLT is true. (This is basically denying a simple proof of Theorem 3,
although we can prove it by using Fermat-Wiles to prove FLT and then note
that both sides of the iff are true....) The issue is that if we suppose
FLT to be false, then we have a V=T=P solution to the first equation of
2.10, but the second equation has $$V^2-T^2=Z_1^2Q^2$$ which has no
solutions with $$Q\ne 0$$ since the LHS is zero and the RHS is positive.
So a counterexample to FLT does not give us an integer solution to 2.10 and
hence equation (8), and even if .
—
Reply to this email directly, view it on GitHub
<#74 (reply in thread)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/BIHIFVFEKRBUQC5V7UENL63ZAPO3FAVCNFSM6AAAAABHCBP65OVHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM4TGMBYHE3TS>
.
You are receiving this because you commented.Message ID:
***@***.***
com>
|
Beta Was this translation helpful? Give feedback.
This comment was marked as off-topic.
This comment was marked as off-topic.
-
Hi friends, |
Beta Was this translation helpful? Give feedback.
-
Pls check the following code for my step sum definition:
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.BigOperators
namespace SumOperator
…-- Define the basic index, scale factor (rho), step, and the sum
operation
def scaleFactor (ρ : ℝ) : ℕ → ℝ
| n => n * ρ
def step (ρ : ℝ) (idx : ℕ) : ℝ :=
scaleFactor ρ idx
def generalizedSum (f : ℝ → ℝ) (ρ : ℝ) (LL UL : ℝ) : ℝ :=
let n_steps := Nat.floor ((UL - LL) / ρ)
let idx_seq := List.range (n_steps + 1)
List.sum (idx_seq.map (λ i => f (LL + step ρ i)))
-- Some examples of applying the generalized sum
def exampleFunction1 (x : ℝ) : ℝ := x^2 + 2*x + 1
def exampleFunction2 (x : ℝ) : ℝ := sin x
#eval generalizedSum exampleFunction1 (1.0 / 2) 0 2 -- Summation with
step = 1/2
#eval generalizedSum exampleFunction2 (π / 4) 0 π -- Summation with
step = π/4
end SumOperator
Il 2024-08-06 13:04 Kevin Buzzard ha scritto:
You formalise it in Lean, I'll believe it.
--
Reply to this email directly, view it on GitHub [1], or unsubscribe
[2].
You are receiving this because you commented.Message ID:
***@***.***>
Links:
------
[1]
#74 (comment)
[2]
https://github.com/notifications/unsubscribe-auth/BKBSWSOSJCOI47CQCXSD5OLZQCUSRAVCNFSM6AAAAABHCBP65OVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTAMRVGI3DAOI
|
Beta Was this translation helpful? Give feedback.
-
New link to the video here (thanks to some hacker my old YT channel was closed...): Fermat the Last Theorem proof via New Sum properties https://www.youtube.com/watch?v=2GzU8rALZh0 Thanks for checking and sharing. It already has a doi and it is well known I'm on from long time ago... |
Beta Was this translation helpful? Give feedback.
-
Dear Sir/Madam, I am sending you my article as my friends have suggested. I will now present my friend's speech from the IAEA: Fermat's Theorem - A Proof by Fermat Himself The Russian nuclear physicist Grigoriy Leonidovich Dedenko has reconstructed the original reasoning of Pierre Fermat, which led Fermat to conclude that the sum of two identical natural powers of rational numbers, raised to an exponent greater than two, is not representable. This is known as Fermat's Last Theorem. As you may know, in 1637, Fermat wrote a note in the margins of his copy of Diophantus's "Arithmetic" stating his discovery and adding, "I have discovered a truly marvelous proof, but this margin is too narrow to contain it." According to G.L. Dedenko, Fermat analyzed power differences using a method that was novel at the time: decomposing these differences into a sum of pairwise products, later known as the "Newton binomial". Fermat discovered that the coefficients in this expansion satisfied simple conditions equivalent to a logarithmic equation (a concept still developing in the mid-17th century) for the degree of the sum (or difference). This equation has only two solutions: the numbers one and two. Thus, the margins of the book were indeed too narrow to contain the complete proof. Fermat's proof would have required the introduction and development of new concepts, such as expansion with combinatorial coefficients (Newton's binomial) and logarithms. It remains unclear whether Fermat ever wrote down his detailed reasoning, and if so, whether this record survives in an unexpected archive. Historians of natural history are encouraged to search anew. Sincerely, Grigoriy Dedenko The final version №25 is available at this link: |
Beta Was this translation helpful? Give feedback.
-
Dear colleagues,
https://osf.io/preprints/osf/jbdas
"The original proof of Pierre Fermat's famous theorem, reconstructed after
35 years of work.
17th-century elementary mathematics. Verified in a simplified version using
Coq and in full using other neural networks.
вт, 23 июл. 2024 г. в 09:46, Complicate-Modulus ***@***.***>:
… Hi friends,
My final Wonderful and Simple FLT Proof hereafter is based on the
Telescoping Sum property. So any student knowing Sum, Limit and Calculus
can follow it, really understanding why Fermat & Wiles are right, still if
they have no ide aof what a Ring is. Representing Powers as Sum of Integers
like A^n=\sum_{1}^{A}(X^n-(X-1)^n) one can start to work with any power
problem (Beal too). But I finally discover that we don't know all the
properties for the Summand Operator (we know how to cut, and how to shift
the limits but no more !), then I first develop and prove 2 new rules:
Scaling and Stretching. Scalig is a new property allow us to mover Step=1/K
instead of mute integer index i just. It shows that just a Power of an
Integer is K invariantive, it means it not depeds on how fine 1/K is in the
Sum we use to represent it: so integer step, rational step 1/K or pushing
the Sum to the limit for k to infility, so step dx the result of the Sum is
always f.ex. A^3. Then I was able to represent Fermat The Last as 2 sums
from 1 to A one for sure representing A^n, the other one C^n-B^n, in where
A,B,C since limits of a finite integer Sum are for sure Integers. So the
final proof comes once one understand that beeing a power of an integer
(f.ex. a cube) means it must be a K invariantive structure, so do not
depends on its numerical value. The first simple prooffor the case n=2
prove Pitagora is right, the following one for n=3 and n=5 shows that
Fermat-Wiles are right since working with C^3-B^3 (or at the 5th power)
like it is a genuine power, means a K invariantive Summation, produce the
absurdum we are looking for: rising the "neutral" K we choose, f.ex.
A^{3m}/A^{3m}, the result for C^3-B^3*(A^{3m}/A^{3m}) once rewriteen in sum
taking the factor A^3m into the upper limit as A^m multiplier, and the
1/A^3m factor as divisor of any term of the Sum, produce a K varinative
result: rising m, the resulg go closer and closer to a diferent integer
from C^n-B^n we start from. Once one understand all this new Complicate
Modulus Algebra (a two hand clock modulat math) one can understand (I hope)
the final more wonderful 1 line proof . For what Beal theorem proof
follows. Here the link:
https://www.researchgate.net/publication/382328938_A_new_useful_denition_for_the_Sum_Operator
—
Reply to this email directly, view it on GitHub
<#74 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AO3HCNVKKD2FSHN7L4AUVQLZNX34LAVCNFSM6AAAAABHCBP65OVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTAMJSGI3DAMI>
.
You are receiving this because you commented.Message ID:
***@***.***
com>
|
Beta Was this translation helpful? Give feedback.
-
The Fermat's Last Theorem Project
Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.
Introduction
Fermat's Last Theorem (FLT) is the claim that some abstract equation has no solutions in positive integers.
Th
https://leanprover-community.github.io/blog/posts/FLT-announcement/
Beta Was this translation helpful? Give feedback.
All reactions