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 inheritance is the assumption that the father is promising at least 1/2, 1/3, and 1/9 of the flock to the respective sons, not the exact fraction. There's a solution where each son gets what's promised, and then a little more.

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 suggestions by adding screenRect.w to the pointer each iteration to avoid the multiplication: https://godbolt.org/z/YfroqK7T6

Writing anything but pixels[y*screenRect.w + x] in an attempt to be faster, without checking the assembly first, is obfuscation.

(For what it's worth, you can beat the compiler by using *pixels++. I didn't profile the code to check it actually was faster in practice however.)

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 (these are subspaces W such that TW is a subset of W). The smallest non-trivial T-invariant subspaces are always 1- or 2-dimensional(!). The first case corresponds to eigenvectors, and T acts by scaling by a real number. In the second case, there's always a basis where T acts by scaling and rotation. The set of all such 2D scaling/rotation transformations are closed under addition, multiplication, and the nonzero ones are invertible. This is the complex numbers! (Correspondence: use C with 1 and i as the basis vectors, then T:C->C is determined by the value of T(1).)

2. Topology: The fact the complex numbers are 2D is essential to their fundamentality. One way I think about it is that, from the perspective of the real numbers, multiplication by -1 is a reflection through 0. But, from an "outside" perspective, you can rotate the real line by 180 degrees, through some ambient space. Having a 2D ambient space is sufficient. (And rotating through an ambient space feels more physically "real" than reflecting through 0.) Adding or multiplying by nonzero complex numbers can always be performed as a continuous transformation inside the complex numbers. And, given a number system that's 2D, you get a key topological invariant of closed paths that avoid the origin: winding number. This gives a 2D version of the Intermediate Value Theorem: If you have a continuous path between two closed loops with different winding numbers, then one of the intermediate closed loops must pass through 0. A consequence to this is the fundamental theorem of algebra, since for a degree-n polynomial f, when r is large enough then f(r*e^(i*t)) traces out for 0<=t<=2*pi a loop with winding number n, and when r=0 either f(0)=0 or f(r*e^(i*t)) traces out a loop with winding number 0, so if n>0 there's some intermediate r for which there's some t such that f(r*e^(i*t))=0.

So, I think the point is that 2D rotations and going around things are natural concepts, and very physical. Going around things lets you ensnare them. A side effect is that (complex) polynomials have (complex) roots.

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 *>, which lets you choose which value you want:

  Just A <* Just B = Just A
  Just A *> Just B = Just B

(There's the possibility to merge values too, with f <$> Just A <*> Just B, which evaluates to Just (f A B). I feel like this is a "don't try to understand it, just get used to it" sort of syntax. It can be pretty convenient though.)

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-additive due to an interaction of specific characteristics of the liquids. Somehow, some connect sums of particular knots enable possibilities that let it more easily be unknotted.

I spent the better part of the summer during grad school trying to prove additivity of unknotting numbers. (I'll mention that it's sort of a relief to know that the reason I failed to prove it wasn't because I wasn't trying hard enough, but that it was impossible!)

One approach I looked into was to come up with some different analogues of unknotting number, ones that were conceptually related but which might or might not be additive, to at least serve as some partial progress. The general idea is represent an unknotting using a certain kind of surface, which can be more restrictive than a general unknotting, and then maybe that version of unknotting can be proved to be additive. Maybe there's some classification of individual unknotting moves where when you have multiple of them in the same knotting surface, they can cancel out in certain ways (e.g. in the classification of surfaces, you can always transform two projective planes into a torus connect summand, in the presence of a third projective plane).

Connect summing mirror images of knots does have some interesting structure that other connect sums don't have — these are known as ribbon knots. It's possible that this structure is a good way to derive that the unknotting number is 5. I'm not sure that would explain any of the other examples they produced however — this is more speculation on how might someone have discovered this counterexample without a large-scale computer search.

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 really the whole thing probably should be scrapped and they should start over.

It's a bit frustrating because, before Copilot, new users would come with proofs and you could spend some time helping them write better proofs and they'd learn things and gain skills, but now it's not clear that this is time well spent on my part. Copilot is not going to learn from my feedback.

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

Something people outside of mathematics don't tend to appreciate is that mathematicians are usually thinking deeply about what we already know, and that work reveals new structures and connections that clarify existing knowledge. The new understanding reveals new gaps in understanding, which are filled in, and the process continues. It's not just about collecting verifiably true things.

Even if somehow the OpenAI algorithm could apply here, we'd get less value out of this whole formalization exercise than to have researchers methodically go through our best understanding of our best proof of FLT again.

> 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 depend on the reduction properties of quotient types in the large scale.

Mathematical reasoning in Lean is almost universally done with rewriting, not reduction. People have found reduction based proofs (colloquially "heavy rfls") to be difficult to maintain. It exposes internal details of definitions. It's better to use the "public API" for mathematical definitions to be sure things can be refactored.

Really, quotients almost should never use the actual `Quot` type unless you have no better choice. In mathematics we like working with objects via universal properties ("public API"). A quotient type is any type that satisfies the universal property of a quotient. All `Quot` does is guarantee that quotients exist with reasonable computation properties, if we ever need them, and if we need those computation properties — which in the kind of math that goes into FLT we often don't. We don't even need `Quot` for Lean to have quotient types, since the classic construction of a set of equivalence classes works. (Though to prove that this construction is correct surely uses functional extensionality, which is proved using `Quot` in some way, but that's an implementation detail of `funext`.)

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 place where the rewrite should occur, with a widget interface to add these position strings by clicking on them in the Infoview. The whole occurrences interface will also be revamped, and maybe someone from the community could help make a widget interface for that too.

Of course there's already `conv => enter [1,3,2]; rw thm`, but putting it directly into `rw` is more convenient while also being more powerful (`conv` has intrinsic limitations for which positions it can access).

The interface is what people will notice, but technical idea of the project is to separate the "what" you want to rewrite from "how" to get dependent type theory to accept it, and then make the "how" backend really good at getting rewrites to go through. No more "motive not type correct", but either success or an error message that gives precise explanations of what went wrong with the rewrite.

And, yeah, it's great that Lean lets you write your own tactics, since it lets people write domain-specific languages just for solving the sorts of things they run into themselves. There's no real difference between writing tactics as a user or as part of the Lean system itself. Anyone could make a new rewrite tactic as a user package.

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 the data for inspection [2], or to independently check that the expressions are type correct and the environment is well-formed (that is, check the correctness).

[1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib

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 with the fully elaborated definitions and theorems. These can be rechecked by the kernel, or by external verifiers. There's no need to trust the Lean system itself, except to make sure that the theorem statements actually correspond to what we think they're supposed to be.

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; the reduction rules are a lot harder to get into.)

> the rewrite (rw) tactic syntax doesn't feel natural either.

Do you have any thoughts on what a natural rewrite syntax would be?

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 system, but it seems to be pretty different from https://users.cs.utah.edu/plt/scope-sets/ (And to clarify what I wrote previously, each identifier has a list of macro scopes.)

The set-of-scopes in Lean 4 is for correct expansion of macro-creating-macros. The scopes are associated to macro expansions rather than binding forms. Lean's syntax quotations add the current macro scope to every identifier that appears in quotations in the expansion. That way, if there are multiple expansions of the same macro for example, it's not possible for identifiers in the expansion to collide. There's an example in section 3.2 of a macro macro that defines some top-level definitions.

(Section 8 of the paper, related work, suggests that set-of-scopes in Lean and Racket are closer than I'm understanding; I think what's going on is that Lean has a separate withFreshMacroScope primitive that macros can invoke, and syntax quotations participate in macro scopes, whereas Racket seems to give this responsibility to binding forms, and they're responsible for adding macro scopes to their binders and bodies. I'm a bit unclear on this.)

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 identifiers created by macros be distinct from any previously created identifiers (the current macro scope is some global state that's incremented whenever a macro is being expanded) — an identifier with this annotation is called a hygienic identifier, and when identifiers are tested for equality the annotations are tested too. With this system in place, there's nothing special you need to do to elaborate binders (and it also lets you splice together syntaxes without any regard for hygiene!). For example, `fun x => b x` elaborates by (1) adding a variable `x` to the local scope, (2) elaborating `b x` in that scope, and then (3) abstracting `x` to make the lambda. The key here is that `x` is a hygienic identifier, so an `x` that's from a different module or macro scope won't be captured by the binder `x`.

Yes you can define the syntax that's in the article in Lean. A version of this is the Mathlib `notation3` command, but it's for defining notation rather than re-using the function name (e.g. using a union symbol for `Set.iUnion`), and also the syntax is a bit odd: notation3 "⋃ "(...)", "r:60:(scoped f => iUnion f) => r

The ideas in the article are neat, and I'll have to think about whether it's something Lean could adopt in some way... Support for nested binders would be cool too. For example, I might be able to see something like `List.all (x in xs) (y in ys) => x + y < 10` for `List.all (fun x => List.all (fun y => x + y < 10) ys) xs`.

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.

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.io/papers/mathlib-paper....

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)

Some links here seem to be broken at the moment — and David's currently on vacation so they likely won't be fixed until January — but if you see for example https://lean-lang.org/basic-types/strings/ it's supposed to be https://lean-lang.org/doc/reference/latest/basic-types/strin...

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 some point you get so used to a definition that even if you don't know a particular formulation word for word, you could still write a textbook on the subject because you know how the theory is supposed to go.

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 students will be CS majors, so the math will be for training rather than an end). Even at the highest levels the definitions are of prime importance, though I suppose once you get to "stage 3" in Terry Tao's classification (see elsewhere in the thread) definitions can start to feel inevitable, since you know what the theory is about, and the definitions need to be what they are to support the theory.

Personal aside: In my own math research, something that's really slowed me down was feeling like I needed everything to feel inevitable. It always bugged me reading papers that gave definitions where I'm wondering "why this definition, why not something else", but the paper never really answers it. Now I'm wondering if my standards have just been too high, and incremental progress means being OK with unsatisfactory definitions... After all, it's what the authors managed to discover.

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, they might have unexpected pathological examples, etc.), and it's the result of lots of hard work by lots of mathematicians throughout history that we have the definitions we enjoy the use of today.

But yeah, while studying math, I think it's similar to learning programming — don't blame the compiler for your mistakes, it's a well-tested piece of software.

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 whether something forms a topological space? Or without knowing the exact definition of continuous, how can you know whether a proof of continuity is correct? Without knowing the definitions, you can't really know mathematics.

To be clear, this does not mean memorizing all the theorems. Getting to know the theorems (and solving problems) is what helps you internalize the subject. Math is the art of what's certain, and knowing exactly what the objects of the subject are is necessary for that. Theorems are derived from the definitions, but definitions can't be derived.

In my experience with a math (undergrad and PhD), I realized I had to know definitions to feel competent at all. In my teaching, it's hard to convince students to actually memorize any definitions — so many times students carry around misconceptions (like that "linearly independent" just means that no vector is a scale multiple of any other vector), but if they just had it memorized, they might realize that the misconception doesn't hold up. Math is weird in that the definitions are actually the exact truth (by definition! tautologically so), so it does take some time to get used to the fact that they're essential.

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 include a formalized proof while we're at it:

  def c (g : β → γ) (f : α → β) (x : α) : γ := g (f x)

  example (h : γ → δ) (g : β → γ) (f : α → β) (x : α) :
      h (g (f x)) = (c (c c) c) h g f x :=
    rfl

  -- Or
  example  :
      (fun (h : γ → δ) (g : β → γ) (f : α → β) (x : α) => h (g (f x)))
        = (c (c c) c) :=
    rfl

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

> 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 uninteresting matter about whether or not you can rw/simp using the theorem due to the statement incidentally containing concrete Decidable instances (it's simply a weakness of these tactics that they are not able to make use of the fact that types are Subsingletons, so if Decidable instances aren't free variables the theorems might not be applicable). There are some old parts of the library that come from probably Lean 2, like Finset, that are fairly constructive, and, since the most developed finite sets are these Finsets, and many of their operations require Decidable instances in their definitions, many theorems about finite sets mention Decidable instances. It's a matter of how much engineering time is available among all the volunteer contributors (along with some fond feelings for Finset since it's been around so long) that we haven't switched over to using the subtype of Set satisfying Set.Finite, which is very non-constructive but would make our lives easier.

I'll emphasize that this rw/simp issue is not about classical reasoning. Even if you banish classical reasoning from the library, it plagues Decidable instances everywhere, and special attention must be made to ensure that theorem statements contain no concrete Decidable instances. Getting this right is an annoying distraction that does not enable any new features or insight.

I'll also emphasize that mathlib theorems do not have Decidable instance hypotheses that are only used in their proofs. Last I checked, there's even a linter for this.

> I don't think that's a fair description of the sibling threads.

Since we're talking about others' "misconceptions", am I right that you weren't aware that in Lean you can do well-founded recursion using a classical termination proof and get a computable function? That's the sort of thing I was trying to make sure we were on the same page about. I brought up LEM to feel out your position because that's what plenty of people mean by constructivism, and I honestly have not been able figure out what constructivism means to you and what sorts of concrete benefits you think constructivist proofs give you. If you're able to interleave a construction with classical reasoning arguing that the construction is well founded, then what is it that the CS and program verification folks are missing from Lean? That's what I'm missing here. (And if there's a good concrete answer the folks who develop Lean itself would be interested.)

To be clear, there are plenty of things missing from Lean that would definitely help CS and program verification folks, but as far as I know none of these features touch upon constructivism.

While I wouldn't say that there are no benefits to constructive reasoning, and I support the work people do on foundations, all these Decidable instances really add to the difficulty that people experience learning to do mathematics in Lean.

I'm sure there are people out there doing program verification that think about it using topos theory, but I suspect it is very few. That's hardly a justification to put resources into making proofs be constructive mathlib-wide.

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!

My observation at the moment is that we haven't seen ML formalize a cutting-edge math paper and that it did in fact take a lot of experience to pull it off so quickly, experience that's not yet encoded in ML models. Maybe one day.

Something that I didn't mention is that Terry Tao is perhaps the most intelligent, articulate, and conscientious person I have ever interacted with. I found it very impressive how quickly he absorbed the Lean language, what goes into formalization, and how to direct a formalization project. He could have done this whole thing on his own I am sure. No amount of modern ML can replace him at the helm. However, he is such an excellent communicator that he could have probably gotten well-above-average results from an LLM. My understanding is that he used tools like ChatGPT to learn Lean and formalization, and my experience is that what you get from these tools is proportional to the quality of what you put into them.

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 is similar to the idea of architecting a large software system by jumping right into writing code. Certainly for small things you can just code it, but past a certain level of complexity you need a plan. Paper is still a useful tool in programming, and theorem proving is just a kind of programming.

During my PhD I occasionally used Lean to check whether some ideas I had made sense. They were more of a technical flavor of idea than what I'd usually think of a novel theorem being, and where Lean was helpful was in keeping track of all these technical details that I didn't trust myself to get completely right.

Speaking of roadmaps, one tool large formalization efforts use are blueprints, an idea developed by Patrick Massot. Here's the one for Tao's project: https://teorth.github.io/pfr/blueprint/dep_graph_document.ht... On this webpage there are also LaTeX versions of every main theorem and links to their Lean equivalents. The original paper was not formal enough to directly formalize in a theorem prover, and this blueprint represents the non-trivial additional creative effort that went into just planning out how to code it.

Speaking of Hoogle, there's Loogle by Joachim Breitner: https://loogle.lean-lang.org/

There's also an AI-driven free-form text tool that recently appeared: https://www.moogle.ai/

A funny thing about libraries saving people from wasting effort redoing things is that, while on one hand this is true that having centralized repositories of knowledge invites people to contribute to them and reuse their work, on the other what can happen is that philosophical differences can cause schisms and result in n-fold duplicated work. (Consider the endless web frameworks out there!) Even Lean could be such a duplication since there's already Coq, Agda, HOL, etc. So far, Lean's mathlib has managed to remain a single project, which I think is an important experiment in seeing if all of mathematics can be unified in a common language. Mathlib is a strange compared to normal software libraries, since its goal is to eventually consume every downstream project that's ever created. If this model can continue to scale, then that makes the question of whether something's been formalized yet or not simpler. Though, even now, there's so much code in mathlib that sometimes you need to go to leanprover.zulipchat.com and ask, and someone familiar with the right corner of the library will usually answer reasonably quickly.

One silver lining for n-fold duplication is that it's usually not a complete reinvention, and this gives variants of ideas an opportunity to explored that otherwise would succumb to the status quo. I feel that even when someone re-formalizes a theorem, it's an additional opportunity to evaluate how this knowledge fits into the larger theory.

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 who isn't concerned about these things.

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 necessarily defeq, so if the wrong instances are present (such as the classical ones) then you need simp-like automation to rewrite instances before unifying. Maybe this is what you're seeing?

There have also been attempts to make polynomials computable, which peppers everything with decidability, but it's not a good data type for real large-scale computations, so it's not clear what the future is there. Maybe the defeqs are worth it, I don't know.

Re constructibility, this is all at too high of a level to really know what you're talking about, or why it's beneficial to write proofs themselves in a certain way. I'm not really even sure what you mean by "constructive". To me, I see no problem with writing a recursive definition that requires a non-constructive proof of termination by well-founded recursion -- is that constructive to you?