Viewing profile — kmill

If someone says they'll pay $8.50 but then they round up and give you $9, you wouldn't say they didn't give you the $8.50 due, right? It's in the $9. I think implicitly with the in…

Certainly check the assembly, but loop invariant code motion and strength reduction are basic optimizations. C compilers tend to be good at optimizing indexing patterns even at -O1…

I'd be surprised if the compiler didn't make that optimisation on its own.

Would you mind sharing your representation? :-)

1. Algebra: Let's say we have a linear operator T on a real vector space V. When trying to analyze a linear operator, a key technique is to determine the T-invariant subspaces (the…

That second operator is the operator, from the Alternative typeclass. The first one has some arbitrariness (do you take the left or right value if both are Just). But, thankfully t…

An analogy might be how if you mix together water and alcohol, you get a solution with less volume than the sum of the volumes. That doesn't mean that there's "negative" volume, ju…

I see people on Zulip using Copilot to write Lean proofs, and they have some success, but the quality is really bad right now, creating long, unmaintainable proofs. New users get s…

My understanding is that the proof doesn't exist in written form in its entirety. Plus, Kevin Buzzard is a world expert with some ideas for how to better organize the proof. In gen…

> I haven't worked with Lean so I don't know how much this crops up in practice It really doesn't. I've been using Lean and Mathlib for about five years now, and Fermat's Last Theo…

We're working on a new rewrite tactic this summer at the Lean FRO (I don't know if I ever directly mentioned that to you yet on Zulip). One interface I'm planning on is `rw [(pos :…

The "olean" files are a binary format that contain everything that was added to the Lean environment. Among other things, it includes all of the declarations and their Lean.Expr [1…

That's Lean 3, from eight years ago, and it's from before 'sorry' really existed in the way we know it now. --- To answer the GP's question: Not only is there a verification mode, …

At least you can 'go to definition' on the tactics and see what they're doing. It's a lot to take in at the beginning, but it can all be inspected and understood. (At least until y…

The system used in Lean 4 is explained in https://arxiv.org/abs/2001.10490v7 (Ullrich and Moura, "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages"). There'…

In Lean's parsed `Syntax`, binders are plain identifiers. The way this works is that identifiers can be annotated with the module it was parsed in as well as a "macro scope", which…

I don't know, but I can do some numerology: a 3:2 aspect ratio that's 512 pixels wide would need a 341 and a third lines, so round up and you get 512 by 342. The later 384 number c…

Kevin Buzzard did great work to popularize mathlib among mathematicians (that's how I got involved myself), but he didn't found mathlib! There's a blurb about the history here: htt…

There's a completely new language reference in the process of being written: https://lean-lang.org/doc/reference/latest/ (by David Thrane Christiansen, co-author of The Little Type…

Yeah, during department teas you can hear mutters of "interesting" as ideas are exchanged and evaluated. But, in my last comment I was just trying to temper my previous comment's c…

I'm teaching discrete math in January — I'll try the analogy, wish me luck! As someone who's gone through the mathematical ringer, the analogy doesn't ring true to me, but it does …

Things get a bit messier once you're doing research mathematics — definitions don't just come from nothing, and a good definition is one that serves its theorems. Definitions can b…

The author really does mean memorize. To engage with pure mathematics, you must know the definitions, since the definitions are the bedrock of the subject. If you don't know the ax…

I used Lean too earlier today :-) I saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also…

Maybe it's translated to English -- a conductor's baton in French is a baguette after all.