markusde

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 you still find Agda friendlier for "normal" fp (and if so, how?)

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 use pure Lean functions and interface with C code across the FFI.

[3] SampCert (AWS). Verified random sampling algorithms for differential privacy. Uses pure Lean functions and is called into via the reverse FFI.

Full disclosure I worked on 2 and 3 haha. There's also some stuff being used by cryptocurrency people but I don't follow that very closely.

[1] https://www.microsoft.com/en-us/research/blog/rewriting-symc... [2] https://github.com/leanprover/KLR [3] https://github.com/leanprover/SampCert

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 like Rust. The disadvantage of the latter is that the Lean model of Rust has to be trusted.

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 example, the semantics of raw pointers in Rust are intentionally under-defined because the compiler writers want to keep changing it.

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.

it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

To me, this sounds like when we first went to the moon, and people were sure we'd be on Mars be the end of the 80's.

Even ARC-AGI-2 is now at over 50%.

Any measure of "are we close to AGI" is as scientifically meaningful as "are we close to a warp drive" because all anyone has to go on at this point is pure speculation. In my opinion, we should all strive to be better scientists and think more carefully about what an observation is supposed to mean before we tout it as evidence. Despite the name, there is no evidence that ARC-AGI tests for AGI.

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, ridiculous.

But speaking as a specialist in theorem proving, this result is pretty impressive! It would have likely taken me a lot longer to formalize this result even if it was in my area of specialty.

Very cool to see how far things have come with this technology!

Please remember that this is a theorem about integers that is subject to a fairly elementary proof that is well-supported by the existing Mathlib infrastructure. It seems that the AI relies on the symbolic proof checker, and the proofs that it is checking don't use very complex definitions in this result. In my experience, proofs like this which are one step removed from existing infra are much much more likely to work.

Again though, this is really insanely cool!!

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 approach to simulate arbitrarily precise samples from the continuous normal distribution.

[1] https://dl.acm.org/doi/10.1145/2710016

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. There's nothing linking theorem prover definitions to pen and paper definitions in any formal system.

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 the latter style a lot more for my work for a couple reasons:

- Fewer side conditions: Setting a / 0 = 0 means that some laws hold even when a denominator is 0, and so you don't need to prove the denominator is nonzero. This is super nice when the denominator is horrible. I heard once that if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions (though I didn't track down this paper to find out for sure).

- Some of the wacky junk arithmetic values, especially as it relates to extended reals, do show up in measure theory. Point being: "junk arithmetic" is a different mathematical theory than normal math, but it's no less legitimate, and is closely related.

- Definition with Hilbert's epsilon operator. If I want to define a function that takes eg. a measurable set S as an argument, I could do the dependent types way

def MyDef (S) (H : measurable S) := /-- real definition -/

but then I need to write all of my theorems in terms of (MyDef S H) and this can cause annoying unification problems (moreso in Rocq than in Lean, assuming H is a Prop). Alternatively, I could use junk math

def MyDef' (S) := if (choose (H : measurable S)) then /-- real definition -/ else /-- junk -/

I can prove (MyDef' S = MyDef S H) when I have access to (H : measurable S). And the property H here can be be really complex, convergence properties, existence properties, etc. It's nice to avoid trucking them around everywhere.

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 seems not very important and porting any enough math to sustain Litex seems like a huge undertaking.

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

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.

The punchline? Bullet point 3 was wrong (it was a PL assignment and I'm 99% sure the AI was picking up on the word macro and regurgitating facts abut LISP). 0 points all around, better luck next time.

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 with applying formal methods in industry and government) and the talk does a good job at explaining where they've seen value-added from formal methods, and the right kind of formal methods for different applications.

[1] https://www.youtube.com/watch?v=gfvvowAc130

Foq is hilarious, especially given that just today Coq released its website with its new name (Rocq)

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 compilation (same as Rocq and Lean, for example). Does F* have some special way to work directly with realistic source code that these other systems don't?

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 on monadic programming, which I'll admit that I don't understand (but would like to!)

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 about a non-dependent type. This comes with design tradeoffs: some lemmas might expect internalized representations only, some rewrites might only be usable (eg. no horrifying dependent type errors) with externalized representations. For math in particular, which involves rich hierarchies of data structures, your choice about internalization might can impacts about what structures from your mathematical library you can use, or the level of fragile type coercion magic that needs to happen behind the scenes.

The examples in this book are extraordinarily simple, and covers material that many proof assistants were designed to be extremely good at expressing. I wouldn't be surprised if a LLM could automate the exercises in this book completely.

Writing nontrivial proofs in a theorem prover is a different beast. In my experience (as someone who writes mechanized mathematical proofs for a living) you need to not only know the proof very well beforehand, but you also need to know the design considerations for all of the steps you are going to use beforehand, and you also need to think about all of the ways your proof is going to be used beforehand. Getting these wrong frequently means redoing a ton of work, because design errors in proof systems are subtle and can remain latent for a long time.

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 N repeating string in the first N(N!+1) characters of any string.

This is 100% the case. All of the honest-to-god Rust experts I know work on the compiler in some way. Same goes for Lean, which bootstraps from C as well.