korrents

formal proof

Machine-checked mathematics: proof assistants such as Lean, and what changes when correctness is certified rather than refereed.

lean-lang.org ↗

What people on korrents have said about formal proof, newest first — 3 positions from 1 person.

  1. TT

    Terence Tao quoted

    Our readingFormalising a proof in Lean currently takes about ten times the effort of writing it out: doable, but annoying.

    Their wordsSo right now I estimate that the time and effort taken to formalize it, proof is about 10 times the amount taken to write it out. So it's doable, but it's annoying.

    ↗Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472youtube.com 5th of 20 in this recording

    Interesting
  3. TT

    Terence Tao quoted

    Our readingLean and tools like GitHub will let experimental mathematics scale far beyond what one mathematician's spaghetti code allows today.

    Their wordsI think the platform that Lean and other software tools, so GitHub and things like that will allow experimental mathematics to scale up to a much greater degree than we can do now.

    ↗Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472youtube.com 6th of 20 in this recording

    mathematics

    Interesting
  5. TT

    Terence Tao quoted

    Our readingWhen formalising a proof costs no more than writing it, mathematics will flip: papers written in Lean first, and journals refereeing only for significance because correctness is certified.

    Their wordsAnd that's a phase shift, because suddenly it makes sense when you write a paper to write it in Lean first, or through a conversation with AI, which is generally on the fly with you, and it becomes natural for journals to accept.

    ↗Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472youtube.com 9th of 20 in this recording

    mathematics

    Interesting