17 ms·

Lean4 helped Terence Tao discover a small bug in his recent paper

497 points by gridentio 3y ago

gsuuon 3y ago
Is there value in learning verified programming for application developers? I've always been curious but they mostly seem like tools for academics.
- deepsun 3y ago
  I believe the most value is taken when there's an asynchronous system and you need to verify it's correctness. Backend dev For app dev I'd say the main problem is always "what we even need to build?", and then polishing over user experience.
X6S1x6Okd1st 3y ago
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
- mensetmanusman 3y ago
  I have found that good communicators that don’t code can quickly make functional automation. Interestingly, LLMs may end up contributing to more inequality if only the highly skilled can leverage them effectively.
  - marshray 3y ago
    My friend had never written anything more than an Excel formula a few months ago and now he's using GPT-4 to write very nontrivial Python applications and automate large parts of his job. I (having 30 years experience as a professional Software Developer^TM) am begging him to teach me his techniques. Now that you mention it, I met him and we became friends in large part due to his communications abilities.
    - an_aparallel 3y ago
      5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to forego stackoverflow/google to get answers. When the GPT-4 model kicks in - my questions are answered with beautiful clarity...whether or not this technology "hallucinates" or not...without a doubt it's empowered me to learn to program. If it's helped me out of 50% of my ruts - i count that as overwhelmingly positive!
      - heavenlyblue 3y ago
        I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.
        hobs 3y ago
        Phind is just prompt engineering, as is anything sitting on top of anything OpenAI is building right now - if you are doing Q&A then maaaaybe it does some resource augmented generation as well (say, from Stack Overflow or other technical resources) Phind is often recommended to me by programmers who find it produces "better" results than a naive GPT-4 session, but I don't know that anyone has done any real world testing.
        astrange 3y ago
        Nobody knows how LLMs work, much less LLMs behind an OpenAI server API, so that's a hard question.
        melagonster 3y ago
        sorry, everyone is losing their job. we have no chances of living in future.
        an_aparallel 3y ago
  - anonylizard 3y ago
    LLMs CURRENTLY favor the more curious and open individuals (High on openness in big 5 scale). Half of the population is not open, does not want to try new things, unless it leads to very direct and proven benefit. However, over time, the overwhelming benefits of using LLMs will be well understood, and these ladder climbers will absolutely master LLMs, no matter their intelligence. People can become experts at taking exams despite how boring and soul sucking that can be, let alone using something way funner and useful like LLMs.
- strikelaserclaw 3y ago
  gpt4 is amazing, i rarely use google as as starting point for my programming related queries these days.
  - danenania 3y ago
    Especially now that the training cutoff is being moved up to April 2023. Questions requiring more recent results were the main ones I’ve been going back to google for.
  - RealityVoid 3y ago
    Huh, I can't seem to get in the groove of using it, maybe I'm old or something, but it annoys me all the subtle ways it's wrong and I feel I have a much better grasp if I think through it myself supported by Google.
    - popularonion 3y ago
      I get a lot of mileage out of ChatGPT just treating it like an intern who turns around work instantly. You don't expect interns to write perfect code, but they can save you a ton of time if you set them loose on the right problems. For any relatively simple task I can say "Write a Python script to do X" and it will almost always spit out working code, even if it has subtle mistakes. Fixing mistakes is fine and part of the process. I don't have to read StackOverflow posts saying "Do you really want to do X?", or sift through documentation that follows the author's approach of how they want to introduce the material but doesn't directly address my question.
      - amelius 3y ago
        Not OP, but I always want to read the code generated by chatgpt before I run it. And I dislike reading other people's code much more than writing it myself.
  - shusaku 3y ago
    Part of this is that ad infested AI generated blog spam is flooding Google! But it’s also my go to. I also really liked GPT to bring me up to speed on a libraries I’ve never used.
- lulznews 3y ago
  They’re an easy 100x for the elite. Top engineers are now 10000x’ers.
  - rowanG077 3y ago
    I don't think you realize what you are saying here. I agree that it is a large boost but 100x is just too ridiculous to take serious. Do you really believe an engineer can now finish in 20 hours what would have taking them a year before?
    - ghshephard 3y ago
      As someone who uses ChatGPT4 pretty much nonstop all day (I have a monitor dedicated to it) - it's almost certainly a 10-20x in fields I have no knowledge of (writing in languages I've never used, dealing with OS/Kernel/Network constructs that are unfamiliar to me) - I can knock off in an hour what might have taken me a day or two previously - but I don't think I've ever had a task where I could say that I completed in 1 hour what would have taken 100 hours - though I would love to hear of counterclaims from people who have been able to do so - definitely not saying impossible, just that I haven't had that experience yet.
      - pradn 3y ago
        The idea of the 10x programmer can mean 1) someone who produces a ton of code quickly 2) someone who can solve seemingly-intractable problems 3) someone who’s presence on a team improves everyone’s productivity quite a bit 4) someone who chooses technical decisions that save a ton of time down the line.
        amelius 3y ago
        (1) is the generally accepted meaning. The others need different words.
        hobs 3y ago
- colinhb 3y ago
  Agree in part but also I think Terry is such an outlier (though also generous and humble) that it’s hard to extrapolate from this example to a more general case
neeleshs 3y ago
Lean4 looks like a great language. Has anyone used it in production capacity for "normal" products/applications?
- spootydooty 3y ago
  AWS has started using it internally recently, but the biggest Lean software project remains Lean 4 itself, which is almost entirely written in Lean 4 (though not verified except for some index operations and data structures). Galois has used Lean 4 internally, too, and I know of another smaller verification project by a German company for verifying some internals that were very difficult to understand. One reason for lack of adoption is that the verified standard library for programming is still rather small. Fortunately, it is expected to grow much more quickly now that there are developers who are getting paid to work on it and I expect that we will likely see a lot more on this front in the coming years.
clircle 3y ago
Never heard of a mathematical error called a bug before
- hanche 3y ago
  Me neither, but it makes sense to me in the case of an error that is relatively easily corrected. If a proof is fatally flawed, however, I would not use that term.
atomicnature 3y ago
A few years back, I was trying to find out how to reduce mistakes in the programs I write. I got introduced to Lamport's TLA+ for creating formal specifications, thinking of program behaviors in state machines. TLA+ taught me about abstraction in a clear manner. Then I also discovered the book series "software foundations", which uses the Coq proof assistant to build formally correct software. The exercises in this book are little games and I found them quite enjoyable to work through. https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
- samvher 3y ago
  I had the same positive experience with Software Foundations. There is another book somewhat derived from it (if I understand correctly) using Agda instead of Coq: https://plfa.github.io/ https://plfa.github.io/ I haven't had the chance to go through it yet, but it's on my list - I think Agda (and as mentioned by another commenter, Idris) is likely to feel more like a programming language than Coq.
- Genbox 3y ago
  Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model. C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead. The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5]. [1] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [3] https://github.com/microsoft/CodeContracts https://github.com/microsoft/CodeContracts [4] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [5] https://github.com/dotnet/csharplang/issues/105 https://github.com/dotnet/csharplang/issues/105
  - 3y ago
SushiHippie 3y ago
For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Carol Collins chair. https://en.wikipedia.org/wiki/Terence_Tao https://en.wikipedia.org/wiki/Terence_Tao
- deleted 3y ago
  [deleted]
- antonioevans 3y ago
  Field's Medal winner.
  - sriram_sun 3y ago
    nit: Fields Medal (no apostrophe).
- c7b 3y ago
  It's correct that he is a professor at UCLA, but it's also worth mentioning that he's regularly called nicknames like 'greatest mathematician alive' (just try googling that phrase): https://academicinfluence.com/rankings/people/most-influential-mathematicians-today https://academicinfluence.com/rankings/people/most-influenti...
  - yodsanklai 3y ago
    What would make him greater than other fields laureate?
    - jyunwai 3y ago
      Beyond the incredible quality and quantity of his work starting from early in his life, what makes Terence Tao memorable to me, is his approachability and willingness to write advice for mathematicians and math students in a blog: https://terrytao.wordpress.com/career-advice/ https://terrytao.wordpress.com/career-advice/ He also has an active Mastodon, which further makes him more approachable: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao It's rare to see a professional at the top of an academic field remain so encouraging to other people in the field, and work to make their work accessible to colleagues across different levels of mathematical maturity.
GEBBL 3y ago
Is it possible that small bugs or assumptions in a root paper could cascade through referencing papers leading to wildly inaccurate outcomes 5 or 6 papers down the line?
- pfdietz 3y ago
  There was an entire school of mathematicians in Italy that went off the rails with incorrect results. https://en.wikipedia.org/wiki/Italian_school_of_algebraic_geometry https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
- gridentio 3y ago
  https://proofwiki.org/wiki/False_Statement_implies_Every_Statement https://proofwiki.org/wiki/False_Statement_implies_Every_Sta...
- thfuran 3y ago
  I work in medical software and a few years ago fixed a bug that was an incorrect parameter value in a model used for computing diagnostic criteria that had proliferated throughout the literature after seemingly being incorrectly transcribed in one influential paper. The difference was relatively small, but it did make results somewhat worse.
- isaacfrond 3y ago
  More likely, wildly inaccurate outcomes will cause a re-examination of the cited theorems, which will probably flush out the bug. By the way it is not clear to me, if the theorem was false or if only proof was wrong.
  - eigenket 3y ago
    The theorem was mostly correct. As stated it was false, but it was true for n >= 8. If you change some not very interesting constants it becomes true for all n. All you need change is the constants for n < 8.
- lmm 3y ago
  In theory yes. In practice mathematicians tend to have a good instinct for which things are true (although not always - some false theorems stood for decades if not centuries) and will avoid looking into ideas that don't pass the sniff test. Plus if you keep building on the consequences of a false result then you'll likely eventually reach a contradiction, which might inspire you to spot the bug in the original result.
Dudester230602 3y ago
I was worried that Lean4 is a yet another LLM, but it's actually some hard and reliable stuff.
- woolion 3y ago
  "Terry Tao finds ChatGPT very helpful to prove new theorems" would actually be bigger news than this one, IMO.
  - throwalean 3y ago
    "Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.
    - woolion 3y ago
      The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work. So while your point is somewhat true [0], as he mentions that these tools could become good enough to do the formal verification part, it's precisely not the interesting part. See [1] and [2]; in particular some things that are very easy to do in real maths can be very challenging in an automated theorem prover, quoting from [2]: >In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation [...] It's impressive to be able to do such mathematics in Lean/Coq..; at all, but it is very tedious mechanical work [3]. >It was more tedious than I expected, with each line of proof taking about an hour to formalize So I think that rather proves the point of what LLMs are currently good for, and what tools can help for really difficult tasks, rather than invalidate it. [0] https://mathstodon.xyz/@tao/111305365372766606 https://mathstodon.xyz/@tao/111305365372766606 [1] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719 [2] https://mathstodon.xyz/@tao/111259986983504485 https://mathstodon.xyz/@tao/111259986983504485 [3] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719
- 3y ago
deterministic 3y ago
Lean4 is brilliant. Worth digging into as a programmer. Coq, Lean4, Agda etc. made my brain explode in a good way. Making me a better software developer.
- gridentio 3y ago
  I'm kind of interested in how useful Lean4 is as a programming language, and if it's easy to prove things about a program written in Lean. I should probably look into that when I have a minute.
  - ykonstant 3y ago
    Regarding usefulness: Lean is very nice to program in, if you care about pure functional languages; its FFI allows you to incorporate fast C routines very easily if pure Lean is not performant enough or lacks features. However, in some domains, Lean is within a decimal order of magnitude of (not hand-optimized) C; some benchmarks I hand-made recently impressed me. Regarding proving things about programs, no, it is not easy, and the developers do not seem to consider it a core goal of Lean.
    - kmill 3y ago
      The core Lean 4 developers do want proving properties about programs to be easy. In the short term maybe priorities have been elsewhere due to limited resources, but that doesn't mean they do not consider this to be a core goal. My understanding is that there are still some research-level problems here that need to be worked out. (Proving things about do notation is currently a real pain for example.)
    - staunton 3y ago
      > the developers do not seem to consider it a core goal of Lean I guess it depends on who you ask. The original devs of Lean wanted to do "everything" (because that's how you start projects, I guess). Since then it has attracted a lot of mathematicians (especially those working on Mathlib, a library that aspires to formalize "all known math") who are happy to have "algorithm objects" and prove things about them without being able to actually run an algorithm on any input. This goes together with mostly embracing classical logic (which breaks the original and most powerful version of Curry-Howard, which allowed you to extract programs from proofs). However, in practical situations, algorithms extracted in this way tend to be too slow to be useful, so maybe that's not actually a downside for programming purposes. Finally, Lean4 "compiles" to C-code, so at least it is (or can reasonably easily be made) portable. People have been trying to use it for real applications, like the AWS stuff others have linked in this thread.
tux3 3y ago
For people looking for an easy introduction to Lean4, the Natural Number Game is great: https://adam.math.hhu.de/#/g/hhu-adam/NNG4 https://adam.math.hhu.de/#/g/hhu-adam/NNG4 And if you just want to read without playing a game: https://lean-lang.org/theorem_proving_in_lean4/introduction.html https://lean-lang.org/theorem_proving_in_lean4/introduction....
- ohduran 3y ago
  Noob here, how is Lean4 different from TLA+ or Alloy? Is that even a reasonable comparison? Edit: Wrote Allow the first time, good stuff.
  - kaba0 3y ago
    I am absolutely not an expert at either of them, but I believe TLA+ is interested mostly about all the possible ordering of “code”, that models your program, verifying the absence of concurrency bugs. Do correct me if I’m wrong, but Lean is more about total functions/FP code, not sure how well does it handle threading, if at all. It might be more related to the correctness of the actual implementation of a serial algorithm.
  - tux3 3y ago
    I'd say TLA+ is designed more for software people trying to design systems, write down specs, and reason about how the thing behaves dynamically. Lean is used mostly for writing down math proofs, and a lot less for software (although by the Curry–Howard correspondence, math proofs and programs have an equivalence, so the line is a little blurry). Lean has "mathlib", which is like a standard library of formally verified math that people can contribute to and use in new proofs. A big multi-year effort to start formalizing the proof of Fermat's Last Theorem in Lean 4 was approved recently: https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_FLT_talk.pdf https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_F...
    - krsrhe 3y ago
      Lean is for verifying proofs, not writing them. It helps you find mistakes, but doesn’t help you understand or express ideas in a human readable way.
nurkalam 3y ago
[flagged]
forward-slashed 3y ago
Also check out Morph Labs, which is working with Lean to create an AI proof assistant. Cool startup by ex-OpenAI folks. Essentially a strong type system of Lean can help with constrained generation. Thus every token would always lead to some valid (if not correct) proof in Lean, iiuc. Maybe people @ Morph can comment. https://x.com/morph_labs https://x.com/morph_labs
Andrew018 3y ago
[dead]
cubefox 3y ago
I wonder whether we could combine formal proof checkers (like the Lean proof checker) with language models that generate synthetic conjecture-proof pairs in a formal language like Lean. The Lean proof checker could be used to automatically verify whether the synthetic proofs written by the language model are correct. This information could be used to provide an RL reward signal applied to the original language model, which would result in it writing better proofs. (Or we train a new model using the correct synthetic proofs of the previous round as training data.) And then the process repeats. So the model would self-train using its synthetic training data, without further human intervention. We could even make this process more adversarial. First we split the generator language model into two: One which generates conjectures, and one which tries to prove/disprove them in Lean. Then add a predictor model which tries to predict whether a synthetic proof is verified by the Lean proof checker. The lower the predicted probability that the proof will be correct, the more reward gets the proof-generator model if it did indeed provide a correct proof. Finally, we add another model which tries to predict the reward the proof-generator model will get for a given synthetic conjecture. Then the conjecture-generator model is rewarded for conjectures that are predicted to yield a high reward in the proof-generator model. So conjectures that are neither too hard not too easy for the proof-generator model. So we would expect that the whole system would progressively create harder and harder synthetic proofs, which in turn allows for better and better self-training of the proof-generator. It seems this could in principle scale to superhuman ability in generating proofs. The process would be somewhat similar GANs or to self-play in AlphaGo Zero. I think the hard part is the initial bootstrapping part, to get the whole process off the ground. Because the initial training of the generator models has to be done with human provided training data (Lean proofs). But once the synthetic proofs are good enough, the system would self-train itself automatically.
- aSanchezStern 3y ago
  Sounds like you've stumbled into the wonderful world of machine-learning guided proof synthesis! While I don't think the full system you're describing has been built yet, many similar systems and pieces have. In terms of the initial phase of supervised learning on existing proofs to prove new ones, there's TacticToe (https://arxiv.org/abs/1804.00596 https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381 https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794 https://arxiv.org/abs/1907.07794), and Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms), among others. Most of these have some sort of language model within them, but if you're specifically looking for the LLM's that have been big recently, there's GPT-f (https://arxiv.org/abs/2009.03393 https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910 https://arxiv.org/abs/2303.04910), and COPRA (https://arxiv.org/abs/2310.04353 https://arxiv.org/abs/2310.04353), though currently these models don't seem as effective as the specialized non-LLM tools. In terms of using reinforcement learning to learn beyond human written proofs, there's TacticZero (https://openreview.net/forum?id=edmYVRkYZv https://openreview.net/forum?id=edmYVRkYZv), this paper from OpenAI (https://arxiv.org/pdf/2202.01344.pdf https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563 https://arxiv.org/abs/1805.07563), the HOList line of work (https://arxiv.org/pdf/1905.10006.pdf https://arxiv.org/pdf/1905.10006.pdf), and HyperTree Proof Search (https://arxiv.org/abs/2205.11491 https://arxiv.org/abs/2205.11491), as well as some in progress work I'm working on with a team at the University of Massachusetts.
omneity 3y ago
That one of the brightest minds of our generation is able to increase his bandwidth with the combination of LLMs and automated proofs makes me super bullish on this tech combo in the future! It starts with bug-fixing, then supports verification, until it starts propelling new discoveries and push the envelope. We need a term when a dynamic like Moore's Law "infects" a field that had no such compounding properties before. EDIT: There's additional context that Terence Tao is using Copilot to help him learn Lean. As shared by adbachman: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941 Could Terence have done it without Copilot? Sure, but like many of us he might not have initiated it due to the friction of adopting a new tool. I think LLM tech has great potential for this "bicycle for the mind" kind of scenarios.
- aylmao 3y ago
  Lean 4 is a theorem prover, and has nothing to do with LLMs as far as I know though.
- aylmao 3y ago
  Lean 4 is a programming language and theorem prover, and has nothing to do with LLMs as far as I know though.
  - adbachman 3y ago
    the missing context from the previous comment is that Tao used GitHub Copilot to help with learning Lean. He's been writing about it as he goes, most recently: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941
    - omneity 3y ago
      Thanks for adding the clarification. I thought this was more common knowledge. I will update my comment accordingly.
- passion__desire 3y ago
  Not to beat the point: LLMs are compiler for english (natural) language.
ocfnash 3y ago
You can even follow his progress on GitHub here: https://github.com/teorth/symmetric_project/ https://github.com/teorth/symmetric_project/
user3939382 3y ago
I’m really excited about dependent types. I’m expecting we won’t get them for a while though. Dependent Haskell is progressing but apparently it’s hard to retrofit. Idris’ own creator has said he expects it to be a model for other languages, I don’t think it will ever have mainstream adoption. Coq and Agda, F* aren’t really designed to be general purpose. Although the implementation for the compiler is complex, and the syntax can get complex and verbose, to me my requirement is simple: I want to encode everything about input and output that I know. Right now in mainstream languages I often know more about my arguments or output than the type system will allow me to specify.
- valyagolev 3y ago
  I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program. If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have everything proven everywhere...
  - skulk 3y ago
    Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.
    - valyagolev 3y ago
      Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point? What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing
gtirloni 3y ago
Tangent useless comment: while checking this Mastodon instance, I noticed a specific user is spamming the global feed by replying to his own posts every other day. I only saw his posts, mostly, and wondered if this was a personal instance of sorts.
- olddustytrail 3y ago
  Did you notice that the domain is mathstadon.xyz so it's probably a pretty small user base.
  - gtirloni 3y ago
    Yes, I noticed the domain and the small instance, but I missed your point.
pmarreck 3y ago
If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem… Anyway, check out Idris[2], it’s cool for this sort of thing
- SmartestUnknown 3y ago
  Exactly lol. Not sure why everyone is taking the contribution of lean in finding the error so seriously. I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).
tgv 3y ago
Does anyone understand what the proof is about? An improved boundary on the mean of geometric series? And why it's only a problem for n=3, k=2, and not for all k=n-1?
- pa7x1 3y ago
  From a very quick glance at page 6 of https://arxiv.org/pdf/2310.05328.pdf https://arxiv.org/pdf/2310.05328.pdf You can see he is treating the case of k=1,2 with that formula and uses induction to extend it to 1 ≤ 𝑘 ≤ 𝑛 − 2. For k = n - 1 he uses a different bound defined in equation 2.2. So he bypasses the issue.
0xpgm 3y ago
Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase? Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.
- ianandrich 3y ago
  Python's Deal library provides contracts and a small portable formal proofs area of the codebase. Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered. It just works surprisingly well for incrementally building up provable code properties.
  - 0xpgm 3y ago
    Thank you! This is great, sounds like what I'm looking for.
- logicchains 3y ago
  >Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase Running a JavaScript codebase through the Typescript compiler is a lightweight way to do incremental proof checking, albeit it can only check proofs about the soundness of the code.
pama 3y ago
Here is earlier context for how Tao used LLM tools, including GPT-4, to help him in this journey. https://mathstodon.xyz/@tao/111233986893287137 https://mathstodon.xyz/@tao/111233986893287137
syngrog66 3y ago
I found a "bug" in one of Terence Tao's math blog posts too, years ago. I told him about it, he fixed it, and thanked me. I didnt make the front page of Hacker News, of course. lol
- syngrog66 3y ago
  If anyone interested, I went into more detail about it, over in a post on my blog: https://news.ycombinator.com/item?id=38040982 https://news.ycombinator.com/item?id=38040982

497 points by gridentio 3y ago

Is there value in learning verified programming for application developers? I've always been curious but they mostly seem like tools for academics.

deepsun 3y ago
I believe the most value is taken when there's an asynchronous system and you need to verify it's correctness. Backend dev For app dev I'd say the main problem is always "what we even need to build?", and then polishing over user experience.

X6S1x6Okd1st 3y ago

He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people

mensetmanusman 3y ago
I have found that good communicators that don’t code can quickly make functional automation. Interestingly, LLMs may end up contributing to more inequality if only the highly skilled can leverage them effectively.
- marshray 3y ago
  My friend had never written anything more than an Excel formula a few months ago and now he's using GPT-4 to write very nontrivial Python applications and automate large parts of his job. I (having 30 years experience as a professional Software Developer^TM) am begging him to teach me his techniques. Now that you mention it, I met him and we became friends in large part due to his communications abilities.
  - an_aparallel 3y ago
    5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to forego stackoverflow/google to get answers. When the GPT-4 model kicks in - my questions are answered with beautiful clarity...whether or not this technology "hallucinates" or not...without a doubt it's empowered me to learn to program. If it's helped me out of 50% of my ruts - i count that as overwhelmingly positive!
    - heavenlyblue 3y ago
      I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.
      - hobs 3y ago
        Phind is just prompt engineering, as is anything sitting on top of anything OpenAI is building right now - if you are doing Q&A then maaaaybe it does some resource augmented generation as well (say, from Stack Overflow or other technical resources) Phind is often recommended to me by programmers who find it produces "better" results than a naive GPT-4 session, but I don't know that anyone has done any real world testing.
      - astrange 3y ago
        Nobody knows how LLMs work, much less LLMs behind an OpenAI server API, so that's a hard question.
      - melagonster 3y ago
        sorry, everyone is losing their job. we have no chances of living in future.
      - an_aparallel 3y ago
- anonylizard 3y ago
  LLMs CURRENTLY favor the more curious and open individuals (High on openness in big 5 scale). Half of the population is not open, does not want to try new things, unless it leads to very direct and proven benefit. However, over time, the overwhelming benefits of using LLMs will be well understood, and these ladder climbers will absolutely master LLMs, no matter their intelligence. People can become experts at taking exams despite how boring and soul sucking that can be, let alone using something way funner and useful like LLMs.
strikelaserclaw 3y ago
gpt4 is amazing, i rarely use google as as starting point for my programming related queries these days.
- danenania 3y ago
  Especially now that the training cutoff is being moved up to April 2023. Questions requiring more recent results were the main ones I’ve been going back to google for.
- RealityVoid 3y ago
  Huh, I can't seem to get in the groove of using it, maybe I'm old or something, but it annoys me all the subtle ways it's wrong and I feel I have a much better grasp if I think through it myself supported by Google.
  - popularonion 3y ago
    I get a lot of mileage out of ChatGPT just treating it like an intern who turns around work instantly. You don't expect interns to write perfect code, but they can save you a ton of time if you set them loose on the right problems. For any relatively simple task I can say "Write a Python script to do X" and it will almost always spit out working code, even if it has subtle mistakes. Fixing mistakes is fine and part of the process. I don't have to read StackOverflow posts saying "Do you really want to do X?", or sift through documentation that follows the author's approach of how they want to introduce the material but doesn't directly address my question.
    - amelius 3y ago
      Not OP, but I always want to read the code generated by chatgpt before I run it. And I dislike reading other people's code much more than writing it myself.
- shusaku 3y ago
  Part of this is that ad infested AI generated blog spam is flooding Google! But it’s also my go to. I also really liked GPT to bring me up to speed on a libraries I’ve never used.
lulznews 3y ago
They’re an easy 100x for the elite. Top engineers are now 10000x’ers.
- rowanG077 3y ago
  I don't think you realize what you are saying here. I agree that it is a large boost but 100x is just too ridiculous to take serious. Do you really believe an engineer can now finish in 20 hours what would have taking them a year before?
  - ghshephard 3y ago
    As someone who uses ChatGPT4 pretty much nonstop all day (I have a monitor dedicated to it) - it's almost certainly a 10-20x in fields I have no knowledge of (writing in languages I've never used, dealing with OS/Kernel/Network constructs that are unfamiliar to me) - I can knock off in an hour what might have taken me a day or two previously - but I don't think I've ever had a task where I could say that I completed in 1 hour what would have taken 100 hours - though I would love to hear of counterclaims from people who have been able to do so - definitely not saying impossible, just that I haven't had that experience yet.
    - pradn 3y ago
      The idea of the 10x programmer can mean 1) someone who produces a ton of code quickly 2) someone who can solve seemingly-intractable problems 3) someone who’s presence on a team improves everyone’s productivity quite a bit 4) someone who chooses technical decisions that save a ton of time down the line.
      - amelius 3y ago
        (1) is the generally accepted meaning. The others need different words.
        hobs 3y ago
colinhb 3y ago
Agree in part but also I think Terry is such an outlier (though also generous and humble) that it’s hard to extrapolate from this example to a more general case

neeleshs 3y ago

Lean4 looks like a great language. Has anyone used it in production capacity for "normal" products/applications?

spootydooty 3y ago
AWS has started using it internally recently, but the biggest Lean software project remains Lean 4 itself, which is almost entirely written in Lean 4 (though not verified except for some index operations and data structures). Galois has used Lean 4 internally, too, and I know of another smaller verification project by a German company for verifying some internals that were very difficult to understand. One reason for lack of adoption is that the verified standard library for programming is still rather small. Fortunately, it is expected to grow much more quickly now that there are developers who are getting paid to work on it and I expect that we will likely see a lot more on this front in the coming years.

clircle 3y ago

Never heard of a mathematical error called a bug before

hanche 3y ago
Me neither, but it makes sense to me in the case of an error that is relatively easily corrected. If a proof is fatally flawed, however, I would not use that term.

atomicnature 3y ago

A few years back, I was trying to find out how to reduce mistakes in the programs I write. I got introduced to Lamport's TLA+ for creating formal specifications, thinking of program behaviors in state machines. TLA+ taught me about abstraction in a clear manner. Then I also discovered the book series "software foundations", which uses the Coq proof assistant to build formally correct software. The exercises in this book are little games and I found them quite enjoyable to work through. https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

samvher 3y ago
I had the same positive experience with Software Foundations. There is another book somewhat derived from it (if I understand correctly) using Agda instead of Coq: https://plfa.github.io/ https://plfa.github.io/ I haven't had the chance to go through it yet, but it's on my list - I think Agda (and as mentioned by another commenter, Idris) is likely to feel more like a programming language than Coq.
Genbox 3y ago
Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model. C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead. The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5]. [1] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [3] https://github.com/microsoft/CodeContracts https://github.com/microsoft/CodeContracts [4] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [5] https://github.com/dotnet/csharplang/issues/105 https://github.com/dotnet/csharplang/issues/105
- 3y ago

SushiHippie 3y ago

For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Carol Collins chair. https://en.wikipedia.org/wiki/Terence_Tao https://en.wikipedia.org/wiki/Terence_Tao

deleted 3y ago
[deleted]
antonioevans 3y ago
Field's Medal winner.
- sriram_sun 3y ago
  nit: Fields Medal (no apostrophe).
c7b 3y ago
It's correct that he is a professor at UCLA, but it's also worth mentioning that he's regularly called nicknames like 'greatest mathematician alive' (just try googling that phrase): https://academicinfluence.com/rankings/people/most-influential-mathematicians-today https://academicinfluence.com/rankings/people/most-influenti...
- yodsanklai 3y ago
  What would make him greater than other fields laureate?
  - jyunwai 3y ago
    Beyond the incredible quality and quantity of his work starting from early in his life, what makes Terence Tao memorable to me, is his approachability and willingness to write advice for mathematicians and math students in a blog: https://terrytao.wordpress.com/career-advice/ https://terrytao.wordpress.com/career-advice/ He also has an active Mastodon, which further makes him more approachable: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao It's rare to see a professional at the top of an academic field remain so encouraging to other people in the field, and work to make their work accessible to colleagues across different levels of mathematical maturity.

GEBBL 3y ago

Is it possible that small bugs or assumptions in a root paper could cascade through referencing papers leading to wildly inaccurate outcomes 5 or 6 papers down the line?

pfdietz 3y ago
There was an entire school of mathematicians in Italy that went off the rails with incorrect results. https://en.wikipedia.org/wiki/Italian_school_of_algebraic_geometry https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
gridentio 3y ago
https://proofwiki.org/wiki/False_Statement_implies_Every_Statement https://proofwiki.org/wiki/False_Statement_implies_Every_Sta...
thfuran 3y ago
I work in medical software and a few years ago fixed a bug that was an incorrect parameter value in a model used for computing diagnostic criteria that had proliferated throughout the literature after seemingly being incorrectly transcribed in one influential paper. The difference was relatively small, but it did make results somewhat worse.
isaacfrond 3y ago
More likely, wildly inaccurate outcomes will cause a re-examination of the cited theorems, which will probably flush out the bug. By the way it is not clear to me, if the theorem was false or if only proof was wrong.
- eigenket 3y ago
  The theorem was mostly correct. As stated it was false, but it was true for n >= 8. If you change some not very interesting constants it becomes true for all n. All you need change is the constants for n < 8.
lmm 3y ago
In theory yes. In practice mathematicians tend to have a good instinct for which things are true (although not always - some false theorems stood for decades if not centuries) and will avoid looking into ideas that don't pass the sniff test. Plus if you keep building on the consequences of a false result then you'll likely eventually reach a contradiction, which might inspire you to spot the bug in the original result.

Dudester230602 3y ago

I was worried that Lean4 is a yet another LLM, but it's actually some hard and reliable stuff.

woolion 3y ago
"Terry Tao finds ChatGPT very helpful to prove new theorems" would actually be bigger news than this one, IMO.
- throwalean 3y ago
  "Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.
  - woolion 3y ago
    The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work. So while your point is somewhat true [0], as he mentions that these tools could become good enough to do the formal verification part, it's precisely not the interesting part. See [1] and [2]; in particular some things that are very easy to do in real maths can be very challenging in an automated theorem prover, quoting from [2]: >In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation [...] It's impressive to be able to do such mathematics in Lean/Coq..; at all, but it is very tedious mechanical work [3]. >It was more tedious than I expected, with each line of proof taking about an hour to formalize So I think that rather proves the point of what LLMs are currently good for, and what tools can help for really difficult tasks, rather than invalidate it. [0] https://mathstodon.xyz/@tao/111305365372766606 https://mathstodon.xyz/@tao/111305365372766606 [1] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719 [2] https://mathstodon.xyz/@tao/111259986983504485 https://mathstodon.xyz/@tao/111259986983504485 [3] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719
3y ago

deterministic 3y ago

Lean4 is brilliant. Worth digging into as a programmer. Coq, Lean4, Agda etc. made my brain explode in a good way. Making me a better software developer.

gridentio 3y ago
I'm kind of interested in how useful Lean4 is as a programming language, and if it's easy to prove things about a program written in Lean. I should probably look into that when I have a minute.
- ykonstant 3y ago
  Regarding usefulness: Lean is very nice to program in, if you care about pure functional languages; its FFI allows you to incorporate fast C routines very easily if pure Lean is not performant enough or lacks features. However, in some domains, Lean is within a decimal order of magnitude of (not hand-optimized) C; some benchmarks I hand-made recently impressed me. Regarding proving things about programs, no, it is not easy, and the developers do not seem to consider it a core goal of Lean.
  - kmill 3y ago
    The core Lean 4 developers do want proving properties about programs to be easy. In the short term maybe priorities have been elsewhere due to limited resources, but that doesn't mean they do not consider this to be a core goal. My understanding is that there are still some research-level problems here that need to be worked out. (Proving things about do notation is currently a real pain for example.)
  - staunton 3y ago
    > the developers do not seem to consider it a core goal of Lean I guess it depends on who you ask. The original devs of Lean wanted to do "everything" (because that's how you start projects, I guess). Since then it has attracted a lot of mathematicians (especially those working on Mathlib, a library that aspires to formalize "all known math") who are happy to have "algorithm objects" and prove things about them without being able to actually run an algorithm on any input. This goes together with mostly embracing classical logic (which breaks the original and most powerful version of Curry-Howard, which allowed you to extract programs from proofs). However, in practical situations, algorithms extracted in this way tend to be too slow to be useful, so maybe that's not actually a downside for programming purposes. Finally, Lean4 "compiles" to C-code, so at least it is (or can reasonably easily be made) portable. People have been trying to use it for real applications, like the AWS stuff others have linked in this thread.

tux3 3y ago

For people looking for an easy introduction to Lean4, the Natural Number Game is great: https://adam.math.hhu.de/#/g/hhu-adam/NNG4 https://adam.math.hhu.de/#/g/hhu-adam/NNG4 And if you just want to read without playing a game: https://lean-lang.org/theorem_proving_in_lean4/introduction.html https://lean-lang.org/theorem_proving_in_lean4/introduction....

ohduran 3y ago
Noob here, how is Lean4 different from TLA+ or Alloy? Is that even a reasonable comparison? Edit: Wrote Allow the first time, good stuff.
- kaba0 3y ago
  I am absolutely not an expert at either of them, but I believe TLA+ is interested mostly about all the possible ordering of “code”, that models your program, verifying the absence of concurrency bugs. Do correct me if I’m wrong, but Lean is more about total functions/FP code, not sure how well does it handle threading, if at all. It might be more related to the correctness of the actual implementation of a serial algorithm.
- tux3 3y ago
  I'd say TLA+ is designed more for software people trying to design systems, write down specs, and reason about how the thing behaves dynamically. Lean is used mostly for writing down math proofs, and a lot less for software (although by the Curry–Howard correspondence, math proofs and programs have an equivalence, so the line is a little blurry). Lean has "mathlib", which is like a standard library of formally verified math that people can contribute to and use in new proofs. A big multi-year effort to start formalizing the proof of Fermat's Last Theorem in Lean 4 was approved recently: https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_FLT_talk.pdf https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_F...
  - krsrhe 3y ago
    Lean is for verifying proofs, not writing them. It helps you find mistakes, but doesn’t help you understand or express ideas in a human readable way.

nurkalam 3y ago

[flagged]

forward-slashed 3y ago

Also check out Morph Labs, which is working with Lean to create an AI proof assistant. Cool startup by ex-OpenAI folks. Essentially a strong type system of Lean can help with constrained generation. Thus every token would always lead to some valid (if not correct) proof in Lean, iiuc. Maybe people @ Morph can comment. https://x.com/morph_labs https://x.com/morph_labs

Andrew018 3y ago

[dead]

cubefox 3y ago

I wonder whether we could combine formal proof checkers (like the Lean proof checker) with language models that generate synthetic conjecture-proof pairs in a formal language like Lean. The Lean proof checker could be used to automatically verify whether the synthetic proofs written by the language model are correct. This information could be used to provide an RL reward signal applied to the original language model, which would result in it writing better proofs. (Or we train a new model using the correct synthetic proofs of the previous round as training data.) And then the process repeats. So the model would self-train using its synthetic training data, without further human intervention. We could even make this process more adversarial. First we split the generator language model into two: One which generates conjectures, and one which tries to prove/disprove them in Lean. Then add a predictor model which tries to predict whether a synthetic proof is verified by the Lean proof checker. The lower the predicted probability that the proof will be correct, the more reward gets the proof-generator model if it did indeed provide a correct proof. Finally, we add another model which tries to predict the reward the proof-generator model will get for a given synthetic conjecture. Then the conjecture-generator model is rewarded for conjectures that are predicted to yield a high reward in the proof-generator model. So conjectures that are neither too hard not too easy for the proof-generator model. So we would expect that the whole system would progressively create harder and harder synthetic proofs, which in turn allows for better and better self-training of the proof-generator. It seems this could in principle scale to superhuman ability in generating proofs. The process would be somewhat similar GANs or to self-play in AlphaGo Zero. I think the hard part is the initial bootstrapping part, to get the whole process off the ground. Because the initial training of the generator models has to be done with human provided training data (Lean proofs). But once the synthetic proofs are good enough, the system would self-train itself automatically.

aSanchezStern 3y ago
Sounds like you've stumbled into the wonderful world of machine-learning guided proof synthesis! While I don't think the full system you're describing has been built yet, many similar systems and pieces have. In terms of the initial phase of supervised learning on existing proofs to prove new ones, there's TacticToe (https://arxiv.org/abs/1804.00596 https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381 https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794 https://arxiv.org/abs/1907.07794), and Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms), among others. Most of these have some sort of language model within them, but if you're specifically looking for the LLM's that have been big recently, there's GPT-f (https://arxiv.org/abs/2009.03393 https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910 https://arxiv.org/abs/2303.04910), and COPRA (https://arxiv.org/abs/2310.04353 https://arxiv.org/abs/2310.04353), though currently these models don't seem as effective as the specialized non-LLM tools. In terms of using reinforcement learning to learn beyond human written proofs, there's TacticZero (https://openreview.net/forum?id=edmYVRkYZv https://openreview.net/forum?id=edmYVRkYZv), this paper from OpenAI (https://arxiv.org/pdf/2202.01344.pdf https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563 https://arxiv.org/abs/1805.07563), the HOList line of work (https://arxiv.org/pdf/1905.10006.pdf https://arxiv.org/pdf/1905.10006.pdf), and HyperTree Proof Search (https://arxiv.org/abs/2205.11491 https://arxiv.org/abs/2205.11491), as well as some in progress work I'm working on with a team at the University of Massachusetts.

omneity 3y ago

That one of the brightest minds of our generation is able to increase his bandwidth with the combination of LLMs and automated proofs makes me super bullish on this tech combo in the future! It starts with bug-fixing, then supports verification, until it starts propelling new discoveries and push the envelope. We need a term when a dynamic like Moore's Law "infects" a field that had no such compounding properties before. EDIT: There's additional context that Terence Tao is using Copilot to help him learn Lean. As shared by adbachman: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941 Could Terence have done it without Copilot? Sure, but like many of us he might not have initiated it due to the friction of adopting a new tool. I think LLM tech has great potential for this "bicycle for the mind" kind of scenarios.

aylmao 3y ago
Lean 4 is a theorem prover, and has nothing to do with LLMs as far as I know though.
aylmao 3y ago
Lean 4 is a programming language and theorem prover, and has nothing to do with LLMs as far as I know though.
- adbachman 3y ago
  the missing context from the previous comment is that Tao used GitHub Copilot to help with learning Lean. He's been writing about it as he goes, most recently: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941
  - omneity 3y ago
    Thanks for adding the clarification. I thought this was more common knowledge. I will update my comment accordingly.
passion__desire 3y ago
Not to beat the point: LLMs are compiler for english (natural) language.

ocfnash 3y ago

You can even follow his progress on GitHub here: https://github.com/teorth/symmetric_project/ https://github.com/teorth/symmetric_project/

user3939382 3y ago

I’m really excited about dependent types. I’m expecting we won’t get them for a while though. Dependent Haskell is progressing but apparently it’s hard to retrofit. Idris’ own creator has said he expects it to be a model for other languages, I don’t think it will ever have mainstream adoption. Coq and Agda, F* aren’t really designed to be general purpose. Although the implementation for the compiler is complex, and the syntax can get complex and verbose, to me my requirement is simple: I want to encode everything about input and output that I know. Right now in mainstream languages I often know more about my arguments or output than the type system will allow me to specify.

valyagolev 3y ago
I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program. If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have everything proven everywhere...
- skulk 3y ago
  Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.
  - valyagolev 3y ago
    Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point? What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing

gtirloni 3y ago

Tangent useless comment: while checking this Mastodon instance, I noticed a specific user is spamming the global feed by replying to his own posts every other day. I only saw his posts, mostly, and wondered if this was a personal instance of sorts.

olddustytrail 3y ago
Did you notice that the domain is mathstadon.xyz so it's probably a pretty small user base.
- gtirloni 3y ago
  Yes, I noticed the domain and the small instance, but I missed your point.

pmarreck 3y ago

If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem… Anyway, check out Idris[2], it’s cool for this sort of thing

SmartestUnknown 3y ago
Exactly lol. Not sure why everyone is taking the contribution of lean in finding the error so seriously. I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).

tgv 3y ago

Does anyone understand what the proof is about? An improved boundary on the mean of geometric series? And why it's only a problem for n=3, k=2, and not for all k=n-1?

pa7x1 3y ago
From a very quick glance at page 6 of https://arxiv.org/pdf/2310.05328.pdf https://arxiv.org/pdf/2310.05328.pdf You can see he is treating the case of k=1,2 with that formula and uses induction to extend it to 1 ≤ 𝑘 ≤ 𝑛 − 2. For k = n - 1 he uses a different bound defined in equation 2.2. So he bypasses the issue.

0xpgm 3y ago

Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase? Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.

ianandrich 3y ago
Python's Deal library provides contracts and a small portable formal proofs area of the codebase. Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered. It just works surprisingly well for incrementally building up provable code properties.
- 0xpgm 3y ago
  Thank you! This is great, sounds like what I'm looking for.
logicchains 3y ago
>Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase Running a JavaScript codebase through the Typescript compiler is a lightweight way to do incremental proof checking, albeit it can only check proofs about the soundness of the code.

pama 3y ago

Here is earlier context for how Tao used LLM tools, including GPT-4, to help him in this journey. https://mathstodon.xyz/@tao/111233986893287137 https://mathstodon.xyz/@tao/111233986893287137

syngrog66 3y ago

I found a "bug" in one of Terence Tao's math blog posts too, years ago. I told him about it, he fixed it, and thanked me. I didnt make the front page of Hacker News, of course. lol

syngrog66 3y ago
If anyone interested, I went into more detail about it, over in a post on my blog: https://news.ycombinator.com/item?id=38040982 https://news.ycombinator.com/item?id=38040982