[Tainnor]

I have no idea how these things are related.

In any case, to my knowledge, no cipher has ever unconditionally been proven secure except the one time pad. We just have a bunch of conditional security proof that are correct if the underlying assumptions (e.g. factoring primes is hard) are correct. Critically, I think all (?) such proofs only work if P != NP, which still remains unproven.

> 1) FLT may have been proven by Wiles

The "may" is misplaced here. Wiles's proof has been extensively reviewed, just because it hasn't been formalised doesn't mean it's wrong.

[kevinbuzzard]

Indeed. I'm not formalising FLT because I think it might be wrong -- I'm formalising it because I know the proof is correct, and using the project as an excuse to get some modern number theory into Lean's mathematics library. My hope is this will increase the chances that systems like Lean will one day be able to help modern mathematicians.

[DoctorOetker]

> In any case, to my knowledge, no cipher has ever unconditionally been proven secure except the one time pad.

Essentially yes.

> We just have a bunch of conditional security proof that are correct if the underlying assumptions (e.g. factoring primes is hard) are correct.

Again correct.

regarding Wiles proof of FLT: you may enjoy reading:

https://xenaproject.wordpress.com/2024/12/11/fermats-last-th...

I understand you for now lack the information I possess, but from my perspective I can absolutely confirm that FLT is correct, since I have a concise proof of it, which even interested highschoolers would be able to follow.

Even in a world where multiple formalized proofs will exist: who's opinion on the security of modern cryptographic protocols would you be more willing to follow:

those cryptographers who fail to prove FLT on their own, which is 99.999% of cryptographers today

a group of mathematicians that together painstakingly formalize a huge detour to prove it,

or a person who proved FLT on their own, thereby proving Fermat could have done the same, in stark contrast to Wiles who argues that Fermat couldn't have possessed such a proof "since not enough mathematics had developed yet in his era in order to prove it" so to speak?

suppose you find yourself lost in the streets of Tokyo, and ask a Prophessor of Geography how to get to destination X and someone who overhears the conversation the same? The person who overheard the conversation claims the professor is wrong, and offers to ask the shortest path to some closer destination Y. The Prophessor answers to take the bus to the train station, then the train to the airport, then some flight to a city in the jungle, then through some archeological Inca site, then the plane again, then a subway, .... and eventually you may or may not end up at Y. Then the person who overheard and proposed the Y challenge, gives a short concise route a few blocks down, and it proves correct. Which of these 2 people's answer will you trust on the original question X?

Who knows their way "around the block"? Fermat and anyone who comes up with a short proof, or the replaceable-gear-people who's collective answer may or may not result in a proof?

[Tainnor]

> who's opinion on the security of modern cryptographic protocols would you be more willing to follow

I'll follow the people who have actually done work in cryptography. I'm neither under the impression that Wiles himself (or Fermat, if we could resuscitate him!) would have much to say about cryptography, nor do I believe that you have a "simple" proof of FLT.

But in any case you missed the substantial point of my comment: whether or not FLT is true (and no matter how short the proof is) is completely irrelevant to modern cryptography, which relies on entirely different problems (e.g. factoring or discrete logarithms).

[DoctorOetker]

> But in any case you missed the substantial point of my comment: whether or not FLT is true

but that is you missing my point, a person finding a succinct machine verifiable proof demonstrates better knowledge of the basic relationships than a convoluted putative proof

integers, integer powers, primes,... none of that has any bearing on cryptography?