kmill

8 ms·

31.
by kmill 3y ago
Yeah, I can imagine that, and I've used sigma types to carry it out (`Subtype`s in particular, or perhaps custom structures). Why does the proof in the sigma type have to be constructive? Certainly this is the road to "dependently
32.
by kmill 3y ago
I'll mention that the "Lean way" for constructivity is that you write `def`s for constructions. These can depend on classical reasoning for well-typedness if you want (like for being sure a number is in range when indexing an
33.
by kmill 3y ago
Yes, sure, and that's how mathlib usually gets developed, project by project and PRing missing background material. I'm one of the mathlib maintainers, and I wanted to be sure there's acknowledgment here for the years of Boub
34.
by kmill 3y ago
I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support). It's exciting to see how quickly the work was done, but it's worth keeping in mind
35.
by kmill 3y ago
I remember playing this game on an old DOS laptop, even in the early 2000s. This version is demonstrating an interesting gotcha with emulating sound. The old PC speaker hardware ran at over 1 MHz, and it would generate square waves at integ
36.
by kmill 3y ago
If you're wondering about downvotes, it's probably because this is mentioned briefly. > It probably should be using tarfile, but let’s ignore that for the moment.
37.
by kmill 3y ago
I mean, big O comes from that particular branch of math. The whole point of it -- even in CS -- is it's asymptotic analysis. (It's also been long criticized in CS for this deficiency. Usually it's the hidden constant factor,
38.
by kmill 3y ago
Big O is about the eventual behavior for large enough N. An algorithm is O(N^2) is for sufficiently large inputs the running time is < c * N^2, for some fixed constant c. That's a really weak guarantee for practical purposes -- it a
39.
by kmill 3y ago
I remember the novel putting a lot of emphasis on how Hammond was a charlatan grifter and would lie about what could be done with genetic engineering (including his lies to raise money when starting the company). There's even doubt abo
40.
by kmill 3y ago
We essentially implemented this matrix version in Lean/mathlib to both compute the fibonacci number and generate an efficient proof for the calculation. https://github.com/leanprover-community/mathlib4/blob&#x
41.
by kmill 3y ago
Yes, I believe so, up to some multiplicative factor. You can carry out the exponentiations in the field Q[sqrt(5)], which is two-dimentional over Q. The interesting thing here is that diagonalization is trading one 2d vector space for anoth
42.
by kmill 3y ago
You're not missing anything. I was going to mention this but decided not to get into it. (One detail: you can't verify the kernel exactly because of Gödel incompleteness issues.)
43.
by kmill 3y ago
The core Lean 4 developers do want proving properties about programs to be easy. In the short term maybe priorities have been elsewhere due to limited resources, but that doesn't mean they do not consider this to be a core goal. My und
44.
by kmill 3y ago
Leo de Moura wants Lean 4 to be used for software verification too. A cool thing about Lean 4 is that it's also a programming language, using the same syntax as for proofs, making it easy to consider proving correctness properties of p
45.
by kmill 3y ago
Lithotripsy has been used for kidney stones since the 1980s. https://www.hopkinsmedicine.org/health/treatment-tests-and-t...
46.
by kmill 3y ago
Ah, you mean "délicieux" or "excellent" ;-)
47.
by kmill 3y ago
I've had to change my terminal colors to be more pastel to nearly eliminate the effect when I'm wearing glasses. I found it to be too distracting, especially since slightly turning my head would make blue text move around!
48.
by kmill 3y ago
That's perfectly fine Haskell, but I wouldn't say that using Applicative is much of a Lean idiom. Especially in the mathlib, people prefer using custom notation that looks like math notation or using the underlying functions direc
49.
by kmill 3y ago
That's not exactly clear to mathematicians, who tend to complain about the "ascii art operators". I think you'll usually see def byTwo (inputList : List.Nat) := inputList.map (. \* 2) rather than using `<$&gt
50.
by kmill 3y ago
Here's an extensible one I wrote a while back for just List, but I haven't tested it in a while: declare_syntax_cat compClause syntax "for " term " in " term : compClause syntax "if " te
51.
by kmill 3y ago
Yeah, and a very big difference between Lean and projects such as the LHC or the James Web telescope are that the LHS and the James Web are massive taxpayer-funded projects, so there is an expectation that their significance is clearly expl
52.
by kmill 3y ago
Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between the two for a little while! The mathlib community has been working on ge
53.
by kmill 3y ago
I use Lean 4 quite a lot these days, and I appreciate how the developers embrace syntax extension and metaprogramming solutions rather than trying to encode complicated control flow using ascii art operators (it's like Lisp meets the M
54.
by kmill 3y ago
Currying is pretty much just a convenient way to write a one-constructor one-method class. It's a parameterized version of the command pattern. That said, if you're using a language with classes you may as well stick with those an
55.
by kmill 3y ago
Even if it's just random noise, if you feed noise into a system you can measure the response and infer properties of the system based on what resonates. I think shouldn't be surprising that if you pay attention to what pops up in
56.
by kmill 3y ago
Oh, thanks for the explanation, I get how it works now. I hadn't seen this trick for an unbounded prime sieve before, and it's a nice idea.
57.
by kmill 3y ago
This allocates a dictionary and the primes() generator for every single prime generated though, so it still has the memory issue, unless there's something I'm missing about how it works?
58.
by kmill 3y ago
The generator is already maintaining a dictionary containing multiple lists that hold all the primes found so far. Even if it instead kept yielding a list of all the primes so far (rather than the most recent prime) it would take less than
59.
by kmill 3y ago
Ok, I see you are trolling. I tip my top hat to you, good day. > Your failure to banish my suspicions despite effort makes me that much more confident in my original conclusion. Side note: I've never considered this phenomenon in my
60.
by kmill 3y ago
This is about understanding something about what goes on as you go rightward on the table at https://en.m.wikipedia.org/wiki/Homotopy_groups_of_spheres (under General Theory) There's an applications section in the

More ›