XPost: sci.math, sci.physics.relativity   
   From: janburse@fastmail.fm   
      
   Hi,   
      
   Is there a Slim Fermats Last Theorem (FLT) but   
   only for Lean4? There is a new proof:   
      
   We formalize a complete proof of the regular   
   case of Fermat's Last Theorem in the Lean4   
   theorem prover. Our formalization includes a   
   proof of Kummer's lemma, that is the main   
   obstruction to Fermat's Last Theorem for   
   regular primes. Rather than following the   
   modern proof of Kummer's lemma via class   
   field theory, we prove it by using Hilbert's   
   Theorems 90-94 in a way that is more   
   amenable to formalization.   
   https://arxiv.org/abs/2410.01466v3   
      
   Is this also available for Rocq or Isabelle/HOL.   
   In as far I feel with ChatGPTs invention of   
   a set theory book:   
      
    > ai: The Incomparable Axioms — Koellner   
   (more philosophical, modern)   
      
   If we have to axiom systems A and B, it is   
   often easy to invoke proof theory and then   
   show A ⊆ B or B ⊆ A. Trouble might start if   
   we want to show A ⊈ B and B ⊈ A,   
      
   this traditional fell into the category of   
   model theory, but modern proof assistants might   
   be better off maybe. Such a proof could be   
   a pebble game, as in EF games,   
      
   or even some things that go beyond EF games.   
   Now for the question whether Rocq or Isabelle/HOL   
   has also a proof, the comparability of Axioms   
   is somehow aggravated, when different proof   
      
   systems have different foundations. What   
   we then need to compare is F+A with G+B,   
   where F and G are the varying foundations.   
   Who said that logic is easy and beautiful?   
      
   Bye   
      
   Mild Shock schrieb:   
   > Hi,   
   >   
   > How it started, DeepSeek:   
   >   
   > me: What are top ten books in set theory?   
   > ai: bla bla   
   > ai: Classic Set Theory: For Guided Independent Study by Derek C. Goldrei   
   >   
   > How its going, ChatGPT:   
   >   
   > me: What are top ten books in set theory?   
   > ai: bla bla   
   > ai: The Incomparable Axioms — Koellner (more philosophical, modern)   
   >   
   > me: Nice try, I don't find "The Incomparable Axioms —   
   > Koellner", you halucinated that   
   >   
   > ai: You’re right — I made a mistake. I hallucinated a   
   > book title. Sorry about that.   
   >   
   > ai: Peter Koellner has written influential papers and   
   > a thesis/lecture notes, but there is no book titled   
   > The Incomparable Axioms by Koellner that I can find.   
   >   
   > The Search for New Axioms   
   > https://dspace.mit.edu/bitstream/handle/1721.1/7989/53014647-MIT.pdf   
   >   
   > LoL   
   >   
   > Bye   
   >   
   > Ross Finlayson schrieb:   
   >> Well, this is quite gratifying, since last year when I got Gemini   
   >> to examine the natural/unit equivalency function the the   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)