kmill

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 typed hell" and it's good to avoid mingling proofs with data if you can, but avoiding the law of the excluded middle doesn't make any of that any easier.

This is also a bit of a distraction since what I really mean regarding TCS is that in my experience is that they do not see the proofs themselves as being objects-with-properties. They're perfectly happy with non-constructive reasoning to support constructions. I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves.

Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs.

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 array), but there is a computability checker. In particular, the compiler sees if there is a way to lower the `def` into some simply typed IR, and this IR can be further compiled to C. If you trust the compiler, then you can trust whether it's real construction.

(Of course, you can also go and prove a definition evaluates to some value if you don't want to trust the evaluator.)

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 Boubaki-style work among hundreds of volunteers to build up the mathematics. In a way, now that the paper's been formalized it's time for the really hard work, which is figuring out how to restructure it (and mathlib) so that it can easily support future work. That's writing libraries for you.

Where are you getting the idea mathlib is being refactored for constructive proofs? I wouldn't say that's on the road map. In fact, the core Lean developers are uninterested in pursuing supporting this.

Since you're here, are you able to say why constructive proofs are interesting to program verification or (T)CS people? I've never heard anyone in TCS even know what constructivity is -- Lean supports their case where you write a program/algorithm and then (with classical logic) prove correctness and other properties. What would constructive logic give them?

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 that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users.

There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one.

Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.

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 integer divisors of this rate. This version of the game is sampling these square waves at 48 KHz, and the jitter from the waves not lining up perfectly adds a bunch of noise known as aliasing artifacts. It's what's giving the music a sort of DTMF (touch tone) quality to it.

I recompiled the game locally with a mitigation for this effect, just by oversampling and taking an average, and it sounds a lot better.

Game Boys also have audio hardware that runs at such high frequencies. I wonder how many emulators run at that rate and downsample properly? High-quality square waves are tricky!

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.

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, but the minimum problem size before it's relevant is an issue too!)

It's fine colloquially misusing big O to mean something like "for usual inputs, the running time is roughly this function", but you can't then in the same breath say all practical algorithms are technically O(1), because that's just not true in the technical sense (and it's useless or at least inaccurate in the colloquial one).

It doesn't really matter, but to add more to the discussion, the way I see it is that computer programs are implementations of algorithms on some restricted set of inputs. The algorithm has the asymptotic analysis, but the program itself does not.

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 allows an algorithm to take stupidly long amounts of time on all practical inputs, so long as eventually it's got a running time with the given bound.

The colloquial use of big O as a general growth factor doesn't hold up to its definition, if you want to be sure it's valid for small inputs too.

I'm in agreement that saying algorithms on computers are all O(1) doesn't make much sense. In a finite memory model, it's impossible to solve big problems, so the running time function becomes undefined for big enough inputs, so big O becomes completely inappropriate in this situation.

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 about exactly how much the park's animals really were resurrected dinosaurs.

It's a compelling modern retelling of The Island of Dr Moreau, but with believable science, and using chaos theory to argue why disaster is inevitable in the unstable system Hammond set up (rather than a mere "he was playing god"). I think it's a cautionary tale of science and engineering without morals. Cutting corners leads to bad science, and there are too many examples of bad science being actively harmful to society. If someone does immoral corner cutting, then who knows what is the depths of their fabrications?

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/master...

In practice this isn't very useful (the definition of Nat.fib unfolds quick enough and concrete large fibonacci numbers don't often appear in proofs) but still it shaves a bit of time off the calculation and the proof verification.

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 another -- one with a very well-behaved multiplication operation (it's distributive, commutative, associative, and invertible).

There's no need to do this to quickly compute fibonacci numbers, but it's pretty neat.

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.)

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 understanding is that there are still some research-level problems here that need to be worked out. (Proving things about do notation is currently a real pain for example.)

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 programs you write. Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).

Lithotripsy has been used for kidney stones since the 1980s.

https://www.hopkinsmedicine.org/health/treatment-tests-and-t...

Ah, you mean "délicieux" or "excellent" ;-)

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!

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 directly rather than by using generic point-free notations. For example, you'll see `⨆ i, s i` for a supremum across the values of `s`, vs a point-free version.

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 `<$>`. There's also `inputList |>.map (. * 2)`, but I haven't seen it in any mathlib theory code yet, just Lean core or in metaprogramming.

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 " term : compClause
    
    syntax "[" term " | " compClause,* "]" : term
    
    macro_rules
      | `([$t:term |]) => `([$t])
      | `([$t:term | for $x in $xs]) => `(List.map (λ $x => $t) $xs)
      | `([$t:term | if $x]) => `(if $x then [$t] else [])
      | `([$t:term | $c, $cs,*]) => `(List.join [[$t | $cs,*] | $c])
    
    #eval [x+1| for x in [1,2,3]]
    -- [2, 3, 4]
    #eval [4 | if 1 < 0]
    -- []
    #eval [4 | if 1 < 3]
    -- [4]
    #eval [(x, y) | for x in List.range 5, for y in List.range 5, if x + y <= 3]
    -- [(0, 0), (0, 1), (0, 2), (0, 3), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (3, 0)]

(Your doElem idea is a good one though)

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 explained to those taxpayers (and scientists want continued funding, so it pays to be clear).

Lean started as a small research project hidden away within Microsoft Research, and mathematicians learned about it and have built a community by word of mouth. There is no accountability needed at all for the project, and there's no need to advertise it -- that's not to say that there hasn't been any effort put into advertising it to mathematicians. I just advertised the system myself an hour ago during a talk that explained Lean and Mathlib to a group of mathematicians, computer scientists, and linguists.

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 getting the documentation to all refer to Lean 4 -- if you find anything old please point it out on the Zulip. There's usually someone around who can fix it relatively quickly.

I think it's better to think of it as bleeding-edge research software rather than alpha software. There might be a little bit of culture shock if you're used to industry-oriented software, but part of this stable version announcement is that there's a new Lean organization that now has resources to improve the experience.

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 ML family). I suppose programming with dependent types is enough of a challenge, so why make it even harder? They've got a sophisticated "do" notation with imperative constructs, mutable variables (that are translated into something StateT-like), and pretty seamless monad lifting. They've also got pipeline operators, including things like `x |>.foo a b c` for `X.foo x a b c` if `x` has type `X` (type-directed field notation is wonderful).

Many times you don't even use currying, since it's not always worth the effort making a particular argument be the last one. Instead you might write `xs.map (f · x)`, where `(f · x)` is short for `fun a => f a x`.

The language also has an interesting GC that lets you write functional algorithms that have good memory performance -- objects with exactly one reference can be mutated (using so-called FBIP, "functional but in-place"). There's an Array type whose theoretical representation is a linked list but whose run-time representation is a dense array with O(1) pushing, popping, and writing. Makes it easy to write performant code without resorting to sophisticated functional data structures.

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 and omit the syntactic sugar from your diet.

I find functional programming useful though because it can shorten code in a way where you can get a better view of the big picture and easily make sweeping changes. But it's also easy to write in a way that's too "perfect" (i.e. resistant to change) and incomprehensible. Though I'm not sure the total incomprehensibility is generally any worse than an enterprise Java codebase -- local readability might only give you the illusion that the whole system is understandable. Still, if you don't enjoy reading code in a certain style it makes for hard reading!

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 dreams you can gain some understanding of our minds. Fourier analysis is just a lot more straightforward than Jungian analysis... and it's made harder from how it's trying to analyze a system from within itself.

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.

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?

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 twice the memory usage.

I'd say the flexibility to not need to know how big of a prime you'll need is the main draw.

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 life, and suddenly other people digging in in the face of evidence makes sense. A dubious "thank you" to you.

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 Wikipedia article, but it's all to other parts of pure math. It's hard to summarize, but they've got to do with obstructions to untangling, unwrapping, or otherwise solving things to do with spaces.