korrents

formal proof

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

lean-lang.org ↗

FilterEveryone, all time19 from 6 people
Group All Technologists 2Scientists 1
Who Everyone HWHillel Wayne 10 MKMartin Kleppmann 3 TTTerence Tao 3 DLDaniel Lemire 1 GSGrant Sanderson 1 TSTim Sweeney 1
When All time Past 1 yearPast 3 yearsPast 5 years
  1. DL

    Daniel Lemire quoted

    Computer science professor who works on fast data processing

    Our readingAI will increasingly produce mathematical proofs, just as it already writes most code.

    Their wordsDifficult proofs will now be built with AI, just as most code will be written with AI.

    ↗The four-colour theorem was only the startlemire.me 2nd of 3 in this piece

  2. 6 weeks earlier
  3. HW

    Hillel Wayne quoted

    Writer and consultant on formal methods

    Our readingFormal methods are not used everywhere because for most real problems writing down what the function should do is itself a nightmare, and a program that is right ninety-nine per cent of the time is good enough.

    Their wordswhen you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases.

    ↗Formal methods with Hillel Wayneyoutube.com 9th of 24 in this recording

  5. HW

    Hillel Wayne quoted

    Our readingNuclear power plants, the standard example of software that must be proved correct, do not care about formal verification: thorough testing is enough for them.

    energynuclear power

    Their wordsbut I can tell you with first hand experience nuclear power plants do not care about this stuff. They're actually just fine with with with thorough testing.

    ↗Formal methods with Hillel Wayneyoutube.com 10th of 24 in this recording

  7. HW

    Hillel Wayne quoted

    Our readingFormal methods shine in highly computational domains and struggle wherever the problem is embedded in human business behaviour.

    Their wordsI think the case of TLA+ and most, not all, but most formal methods, they shine the most in highly computational domains, where most of the problems are highly technical and not like business embedded.

    ↗Formal methods with Hillel Wayneyoutube.com 15th of 24 in this recording

  9. HW

    Hillel Wayne quoted

    Our readingEngineers are sceptical of formal methods because they were burned by CASE and UML, sold as miracle solutions and imposed on them regardless of fit.

    Their wordsI think a lot of the reason people are skeptical of these is because they've been burned by things like case and UML and all these other miracle solutions that were forced on them by people who wanted them to use it no matter what.

    ↗Formal methods with Hillel Wayneyoutube.com 16th of 24 in this recording

  11. HW

    Hillel Wayne quoted

    Our readingFormal methods are a niche tool; property-based testing is the one most engineers should adopt, and stopping there is a fine place to stop.

    Their wordsI love formal methods, but I think it's a fairly niche tool for most people and I think like property-based testing is in general going to be useful for more people.

    ↗Formal methods with Hillel Wayneyoutube.com 17th of 24 in this recording

  13. HW

    Hillel Wayne quoted

    Our readingAI is making formal methods more popular without making them mainstream, moving them from about a tenth of a per cent of engineers to three tenths.

    Their wordsI think it is making it more popular. I don't know if it'll make it go mainstream, but it's definitely making it a lot more popular. It's bringing it from maybe like 0.1% to 0.3% which is huge.

    ↗Formal methods with Hillel Wayneyoutube.com 20th of 24 in this recording

  14. 4 weeks earlier
  15. GS

    Grant Sanderson quoted

    Mathematics explainer, creator of the YouTube channel 3Blue1Brown

    Our readingFormalisation's real gift is the green check mark — knowing a hard proof is correct before you spend time on it — and every other field would kill for it.

    Their wordsAnd so having anything that's able to give you that green check mark that says even if this is going to be complicated to understand, even if it's going to be a pain, you at the very least know it is correct. Like every other field would kill for that, right?

    ↗Grant Sanderson (@3blue1brown) – AI disproved a famous math conjecture. Now what?youtube.com 15th of 23 in this recording

  16. 2 months earlier
  17. MK

    Martin Kleppmann quoted

    Computer science researcher at Cambridge

    Our readingA test checks a handful of examples; a proof settles an infinite state space, which is why formal methods can say things testing never can.

    Their wordsBut a proof can reason about potentially infinite state spaces. So, it can tell you things about like every possible thing that could possibly happen in the entire universe.

    ↗Designing Data-intensive Applications with Martin Kleppmannyoutube.com 17th of 26 in this recording

  19. MK

    Martin Kleppmann quoted

    Our readingFormal verification is about to become economical, because models are getting good enough at writing the proofs that humans no longer have to.

    LLMs

    Their wordsOne is that the LLMs are getting increasingly good at writing these proofs. And if we don't have to write the proof by hand as humans, it just becomes feasible to do them in situations where previously it would have not been economical.

    ↗Designing Data-intensive Applications with Martin Kleppmannyoutube.com 18th of 26 in this recording

  21. MK

    Martin Kleppmann quoted

    Our readingAI-written code makes formal proof necessary, because human review of all that generated code becomes the bottleneck.

    LLMscode generationAI writing

    Their wordsBut also LLMs increase the need for these formal proofs because, you know, we're live coding a bunch of stuff. If we have to manually review all of that code, then that will become the bottleneck.

    ↗Designing Data-intensive Applications with Martin Kleppmannyoutube.com 19th of 26 in this recording

  22. 10 months earlier
  23. 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

  25. 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.

    mathematics

    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

  27. 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.

    mathematics

    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

  28. 6 weeks earlier
  29. TS

    Tim Sweeney quoted

    Founder and CEO of Epic Games

    Our readingThere is one right way to build a type system, the way that gives you mathematical proofs, and every other kind of type system is simply worse and should be rejected.

    Their wordsBut there are other parts of programming languages that are not subjective but should be fundamental. And when you look at type systems, there is a way to do type systems that gives you mathematical proofs. And every other way of type systems that doesn't give you mathematical proofs is just worse and should ultimately be rejected.

    ↗Tim Sweeney: Fortnite, Unreal Engine, and the Future of Gaming | Lex Fridman Podcast #467youtube.com 15th of 22 in this recording

  30. 6 years earlier
  31. HW

    Hillel Wayne quoted

    Our readingFormal methods are not standard practice even in high-assurance software such as medical devices and aircraft.

    Their wordsmost people in high-assurance software don't use formal methods

    ↗Why Don't People Use Formal Methods?hillelwayne.com 1st of 5 in this piece

  33. HW

    Hillel Wayne quoted

    Our readingThe hard part of verification is not proving the code correct but working out what the specification should say.

    Their wordsFinding the right spec is one of the biggest challenges in formal methods.

    ↗Why Don't People Use Formal Methods?hillelwayne.com 2nd of 5 in this piece

  35. HW

    Hillel Wayne quoted

    Our readingThere is a permanent trade-off in verification: an expressive language is hard to prove things about, and a language that is easy to prove things about is hard to write in.

    Their wordsFormal verifiers have a dilemma: the more expressive the language, the harder it is to prove anything in it. But the less expressive the language, the harder it is to write anything in it.

    ↗Why Don't People Use Formal Methods?hillelwayne.com 3rd of 5 in this piece

  37. HW

    Hillel Wayne quoted

    Our readingFull formal verification is a waste of money for most software: near-perfect is reachable with ordinary techniques at a fraction of the cost.

    Their wordsYou do not need full code verification to write good software or even to write near-perfect software.

    ↗Why Don't People Use Formal Methods?hillelwayne.com 5th of 5 in this piece