Viewing profile — markusde

"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 det…

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 mor…

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…

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 intere…

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…

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 WebAssemb…

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 s…

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 solu…

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-supp…

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 …

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…

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 …

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. T…

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 betw…

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 generat…

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 bea…

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 …

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 co…

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