markusde

5 ms·

1.
by markusde 1mo ago
"Complex topics" in this case means reading 22 AI-generated paragraphs that supposedly cover the entire chip manufacturing process. If the author seriously thinks this level of detail is complex then they have psychosis.
2.
by markusde 2mo ago
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...
3.
by markusde 5mo ago
Thanks! Typeclasses are also something I really like about Lean.
4.
by markusde 5mo ago
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 s
5.
by markusde 6mo ago
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
6.
by markusde 6mo ago
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.
7.
by markusde 6mo ago
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 disad
8.
by markusde 7mo ago
It's almost like context matters
9.
by markusde 8mo ago
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
10.
by markusde 8mo ago
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.
11.
by markusde 8mo ago
> 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
12.
by markusde 8mo ago
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.
13.
by markusde 8mo ago
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
14.
by markusde 9mo ago
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
15.
by markusde 9mo ago
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!
16.
by markusde 9mo ago
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 n
17.
by markusde 9mo ago
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 l
18.
by markusde 9mo ago
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!
19.
by markusde 9mo ago
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 impor
20.
by markusde 1y ago
Could you link to any more information about this?
21.
by markusde 1y ago
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.
22.
by markusde 1y ago
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.
23.
by markusde 1y ago
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 p
24.
by markusde 2y ago
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 forma
25.
by markusde 2y ago
Foq is hilarious, especially given that just today Coq released its website with its new name (Rocq)
26.
by markusde 2y ago
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
27.
by markusde 2y ago
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 progr
28.
by markusde 2y ago
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-depen
29.
by markusde 2y ago
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 completel
30.
by markusde 2y ago
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

More ›