Somewhat of a tangent but it is actually called "glorious" in the official docs https://downloads.haskell.org/~ghc/7.4.1/docs/html/users_gui...
Thanks! Typeclasses are also something I really like about Lean.
I'm curious what you like about Agda functional programming? Many of the praises I hear about it have to do with it's dependent pattern matching, and I think Lean suffers a lot more in that regard. I'm curious though if…
In addition to Cedar: [1] SymCrypt (MSR). Verified cryptographic primitives. It's in the latter style, using the Aeneas model of Rust. [2] KLR (AWS). ML compiler. Not verified, but it's in the former style where they…
You should check out the recent PR's to the Agda repo... the community is currently very divided about AI. For better or worse, the people driving the Lean project have been interested in AI for quite some time.
Also a very good question btw, people do both. For some projects Lean is expressive and performant enough to use on its own (or call into using the reverse FFI), other projects use a model of a real programming language…
It's almost like context matters
Yeah, but the problem is that programming languages and compilers change all the time, making it hard to maintain a formal model of them. Exceptions exist (CompCert C and WebAssembly are two good examples) but for…
As is "even if it was in my area of specialty". I would not be able to do this proof, I can tell you that much.
Yes, the contributions of the people promoting the AI should be considered, as well as the people who designed the Lean libraries used in-the-loop while the AI was writing the solution. Any talk of "AGI" is, as always,…
Kind of, but you're not just picking rationals, you're picking rationals that are known to converge to a real number with some continuous property. You might be interested in this paper [1] which builds on top of this…
Exactly right. You can pick and use real numbers, as long as they are only queried to finite precision. There are lots of super cool algorithms for doing this!
You can't prove something untrue (in the sense that it implies false) without proving that the theorem prover is is unsound, which I think at the moment is not known to be possible in Lean. But you're exactly right.…
This is a topic of contention in formalized math with no universal right answer. Some libraries go heavy on the dependent types, and some like mathlib try to avoid them. I do math in both Rocq and Lean and I find I like…
To be honest I'm not convinced by the technical downsides you mentioned here BUT I can see why you wouldn't want to spend time on this if it takes away from language development. Thanks!
One thing I never understood about this: why does this not just compile to Lean so they're compatible with each other? Having a good interface is admirable, but the difference between set and type based foundations…
Could you link to any more information about this?
Proofs, sure, but not definitions. A human needs to be sure that the definitions align with that they expect. Unfortunately, humans generating correct definitions and LLM's generating correct proofs are not independent…
IMO problems are stated in and solved by math a high schooler could understand. Getting the definitions right (one of the harder parts of mechanizing proofs IME) is a different beast altogether.
Preach about the bullet points. I was grading some assignments a while ago and by some mysterious coincidence like a third of the answers were written in this strange bullet point format listing the the same 3 ideas.…
I'd recommend anyone with a passing interest in the role formal techniques can play in software development watch this [1] talk. Mike Dodds is a principal scientist at Galois (a company which has a lot of experience…
Do you think you might be able to elaborate a little bit more about this? I was skimming the "Proof-Oriented Programming" book, and it seems that the primary way to execute F* programs is by extraction or trusted…
One technical difference is that F* heavily uses SMT automation, which is less emphasized in Lean (their book even says that F* typechecking is undecidable). F* programmers frequently talk about the language's emphasis…
The issue is-- there are lots of way to write down a statement. One common example is if you're going to internalize or externalize a property of a data structure: eg. represent it with a dependent type, or a property…
The longest sequence of digits that eventually repeat (as defined in the article) is unboundedly large for any infinite sequence of digits, not just pi! Using the pigeonhole principle, there must be at least one length…
Somewhat of a tangent but it is actually called "glorious" in the official docs https://downloads.haskell.org/~ghc/7.4.1/docs/html/users_gui...
Thanks! Typeclasses are also something I really like about Lean.
I'm curious what you like about Agda functional programming? Many of the praises I hear about it have to do with it's dependent pattern matching, and I think Lean suffers a lot more in that regard. I'm curious though if…
In addition to Cedar: [1] SymCrypt (MSR). Verified cryptographic primitives. It's in the latter style, using the Aeneas model of Rust. [2] KLR (AWS). ML compiler. Not verified, but it's in the former style where they…
You should check out the recent PR's to the Agda repo... the community is currently very divided about AI. For better or worse, the people driving the Lean project have been interested in AI for quite some time.
Also a very good question btw, people do both. For some projects Lean is expressive and performant enough to use on its own (or call into using the reverse FFI), other projects use a model of a real programming language…
It's almost like context matters
Yeah, but the problem is that programming languages and compilers change all the time, making it hard to maintain a formal model of them. Exceptions exist (CompCert C and WebAssembly are two good examples) but for…
As is "even if it was in my area of specialty". I would not be able to do this proof, I can tell you that much.
Yes, the contributions of the people promoting the AI should be considered, as well as the people who designed the Lean libraries used in-the-loop while the AI was writing the solution. Any talk of "AGI" is, as always,…
Kind of, but you're not just picking rationals, you're picking rationals that are known to converge to a real number with some continuous property. You might be interested in this paper [1] which builds on top of this…
Exactly right. You can pick and use real numbers, as long as they are only queried to finite precision. There are lots of super cool algorithms for doing this!
You can't prove something untrue (in the sense that it implies false) without proving that the theorem prover is is unsound, which I think at the moment is not known to be possible in Lean. But you're exactly right.…
This is a topic of contention in formalized math with no universal right answer. Some libraries go heavy on the dependent types, and some like mathlib try to avoid them. I do math in both Rocq and Lean and I find I like…
To be honest I'm not convinced by the technical downsides you mentioned here BUT I can see why you wouldn't want to spend time on this if it takes away from language development. Thanks!
One thing I never understood about this: why does this not just compile to Lean so they're compatible with each other? Having a good interface is admirable, but the difference between set and type based foundations…
Could you link to any more information about this?
Proofs, sure, but not definitions. A human needs to be sure that the definitions align with that they expect. Unfortunately, humans generating correct definitions and LLM's generating correct proofs are not independent…
IMO problems are stated in and solved by math a high schooler could understand. Getting the definitions right (one of the harder parts of mechanizing proofs IME) is a different beast altogether.
Preach about the bullet points. I was grading some assignments a while ago and by some mysterious coincidence like a third of the answers were written in this strange bullet point format listing the the same 3 ideas.…
I'd recommend anyone with a passing interest in the role formal techniques can play in software development watch this [1] talk. Mike Dodds is a principal scientist at Galois (a company which has a lot of experience…
Do you think you might be able to elaborate a little bit more about this? I was skimming the "Proof-Oriented Programming" book, and it seems that the primary way to execute F* programs is by extraction or trusted…
One technical difference is that F* heavily uses SMT automation, which is less emphasized in Lean (their book even says that F* typechecking is undecidable). F* programmers frequently talk about the language's emphasis…
The issue is-- there are lots of way to write down a statement. One common example is if you're going to internalize or externalize a property of a data structure: eg. represent it with a dependent type, or a property…
The longest sequence of digits that eventually repeat (as defined in the article) is unboundedly large for any infinite sequence of digits, not just pi! Using the pigeonhole principle, there must be at least one length…