kmill

5 ms·

1.
by kmill 3mo ago
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 inheritance is the assumption that the fat
2.
by kmill 3mo ago
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. Take a look, GCC and Clang go further than these suggestio
3.
by kmill 3mo ago
I'd be surprised if the compiler didn't make that optimisation on its own.
4.
by kmill 7mo ago
Would you mind sharing your representation? :-)
5.
by kmill 7mo ago
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 (these are subspaces W such that TW is a subset of W). The
6.
by kmill 1y ago
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 the Applicative typeclass gives both <* and *&gt
7.
by kmill 1y ago
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, just that the volume turns out to be sub-a
8.
by kmill 1y ago
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 stuck, thinking they're 90% of the way to the end, but r
9.
by kmill 1y ago
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 general, formalization leads to new understanding about ma
10.
by kmill 1y ago
> 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 Theorem is definitely not going to d
11.
by kmill 1y ago
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 := 1,3,2) thm]` to be able to navigate to the
12.
by kmill 1y ago
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] expressions. People have written tools to dump t
13.
by kmill 1y ago
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, but Lean generates object files wit
14.
by kmill 1y ago
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 you get to the fundamental type theory; t
15.
by kmill 1y ago
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's still a set-of-scopes
16.
by kmill 1y ago
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 is a number that's used to make identif
17.
by kmill 1y ago
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 corresponds to an exact 4:3 aspect ratio.
18.
by kmill 2y ago
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: https://leanprover-community.github.i
19.
by kmill 2y ago
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 Typer, and Lean FRO member)
20.
by kmill 2y ago
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 claim about how important definitions are. At
21.
by kmill 2y ago
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 sound pedagogically useful still (my stu
22.
by kmill 2y ago
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 be "wrong" (they might be generalizable
23.
by kmill 2y ago
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 axioms of a topology, how can you check for yourself wh
24.
by kmill 2y ago
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 stumbled on the c (c c) c solution. May as well i
25.
by kmill 3y ago
Maybe it's translated to English -- a conductor's baton in French is a baguette after all.
26.
by kmill 3y ago
> we want to work with our own assertions about decidability, and not let classical reasoning mess that up I am not confident that you understood what I meant. It has nothing to do with the proofs themselves, but a mathematically uninter
27.
by kmill 3y ago
That's a lot of links to take in, and I don't do really anything with ML, but feel free to head over to https://leanprover.zulipchat.com/ and start a discussion in the Machine Learning for Theorem Proving stream!
28.
by kmill 3y ago
I'm by no means an expert on interactive theorem proving -- I'm just a Lean user who knows a lot about how Lean works, and I got into it while procrastinating finishing my math PhD. I think writing novel theorems directly in Lean
29.
by kmill 3y ago
It's not `noncomputable` in Lean though. Lots of computable functions use it. I've read Bauer's paper before btw. I think topoi are cool, but I don't think it's a complexity worth thinking about for everyone else wh
30.
by kmill 3y ago
Many times, Decidable assumptions are added simply because they appear in the terms in a theorem statement, and doing so makes applying such a theorem easier. There's the technical annoyance that Decidable instances are equal but not n

More ›