3 ms·

I possess a proof of FLT, and will publish the metamath formalization, in due time (first I need to build a secure display, for reasons that will become clear).

olddustytrail 1y ago
Fermat's Last Theorem is easily solved with css. Just do: margin-left: 200px; and you're sorted.
- DoctorOetker 1y ago
  people jest, but they will jest less once they think a little more critically: 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? who knows their way around the block, if the consensus is that Fermat did not possess a proof but Wiles did finally find a proof, who knows their way around the block, if a much more succinct proof than Wiles long-winded-anc-to-this-date-not-formally-verified-proof? would you jest less?
  - olddustytrail 1y ago
    I probably wouldn't. I'm in a jovial mood and I've managed to joke about many of the worst parts of my life. There are many worse things happening in the world than issues in mathematics. You seem in a serious mood but these things too shall pass.
    - DoctorOetker 1y ago
      > There are many worse things happening in the world than issues in mathematics. But mathematics in general and cryptography in specific, and the canon / propaganda that surrounds it is intimately affecting the principal variation of the same events you so lament.
  - Tainnor 1y ago
    > 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 1y ago
      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 1y ago
        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 1y ago
        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.

olddustytrail 1y ago

Fermat's Last Theorem is easily solved with css. Just do: margin-left: 200px; and you're sorted.

DoctorOetker 1y ago
people jest, but they will jest less once they think a little more critically: 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? who knows their way around the block, if the consensus is that Fermat did not possess a proof but Wiles did finally find a proof, who knows their way around the block, if a much more succinct proof than Wiles long-winded-anc-to-this-date-not-formally-verified-proof? would you jest less?
- olddustytrail 1y ago
  I probably wouldn't. I'm in a jovial mood and I've managed to joke about many of the worst parts of my life. There are many worse things happening in the world than issues in mathematics. You seem in a serious mood but these things too shall pass.
  - DoctorOetker 1y ago
    > There are many worse things happening in the world than issues in mathematics. But mathematics in general and cryptography in specific, and the canon / propaganda that surrounds it is intimately affecting the principal variation of the same events you so lament.
- Tainnor 1y ago
  > 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 1y ago
    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 1y ago
      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 1y ago
        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.