> how can cryptography experts expound the security of such and such cryptographic primitives involving discrete numbers, exponentiation, ... but be unable to come up with alternative proofs of FLT? ... but be unable to individually formalize existing supposed proof of FLT? ... but be unable to find a more succinct proof of FLT?

I have no idea why you think there's a contradiction in here somewhere.

▲

DoctorOetker 10 days ago | parent [-]

The question is not if the described behavior is happening, but how credible their claims of cryptographic security are for the cryptographic primitives we depend on en masse.

Apart from unconditional security protocols, the safety of the cryptographic primitives is never proven, but insinuated by the lack of a public disproof.

How can consensus agreement be satisfied with the situation that 1) FLT may have been proven by Wiles 2) But has not been formally verified yet 3) We assume Fermat could not have found a proof, which insinuates that 4) a succinct proof is assumed to be impossible unless 5) we collectively underestimate Fermat / the power of individual human brains / sheer dedication 6) while pretending there is little to no connection between FLT and public key encryption schemes.

▲

Tainnor 10 days ago | parent [-]

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 10 days ago | parent | next [-]

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 9 days ago | parent | prev [-]

> 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 9 days ago | parent [-]

> 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 9 days ago \| parent [-]
		> 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?