Searching a Kevin Buzzard Talk

Stream: general

[Franz Huschenbeth]

I think I have seen somewhere a talk (or Paper?) of Kevin Buzzard on "Can Lean encompass / formalize all of math" or something along these lines. I tried searching for it, but have not found anything. Does someone know of such talk?

If there does not exist a talk like that from Kevin Buzzard, then I would be also interested into other resources on that question.

[Kevin Buzzard]

I don't see why it can't formalize most of maths. There are parts of it for which it would be quite complicated but my favourite parts should be fine.

[Snir Broshi]

I think the 3rd paragraph of #general > sloplib @ 💬 is an interesting take- it means that the answer to your question depends on your definitions of "formalize" and "all".

[Snir Broshi]

Taking the question at face value, i.e. whether dependent types and universes and such break down at some point of fancier and fancier math, then I'd guess that if anything breaks it'll be in category theory (or a similar field with universe concerns, maybe algebraic geometry?).
You might like this talk with Emily Riehl that talks about problems formalizing category theory, or this blog post by the creator of Isabelle about dependent types vs another formalism

[Franz Huschenbeth]

Snir Broshi said:

I think the 3rd paragraph of #general > sloplib @ 💬 is an interesting take- it means that the answer to your question depends on your definitions of "formalize" and "all".

With "all" I meant all math we care about :)

[Franz Huschenbeth]

Snir Broshi said:

Taking the question at face value, i.e. whether dependent types and universes and such break down at some point of fancier and fancier math, then I'd guess that if anything breaks it'll be in category theory (or a similar field with universe concerns, maybe algebraic geometry?).
You might like this talk with Emily Riehl that talks about problems formalizing category theory, or this blog post by the creator of Isabelle about dependent types vs another formalism

I have also thought into that direction of category theory and its good to see that the Infinity Cosmos Project is faring fine with Lean. I guess I am also interested in a model theoretic perspective, in the sense that the strength of Lean is enough for all math we care about. (Disclaimer: I dont know a whole lot on model theory)

[Franz Huschenbeth]

Will look into the blog post, thanks.

[Franz Huschenbeth]

Kevin Buzzard said:

I don't see why it can't formalize most of maths. There are parts of it for which it would be quite complicated but my favourite parts should be fine.

I suppose that means there was no talk of you in that direction :)

[Snir Broshi]

Franz Huschenbeth said:

With "all" I meant all math we care about :)

I didn't mean which math, but rather which parts of the act of doing math. For example, some math is inherently informal, such as discussions where you make a bunch of informal arguments to reach a pseudo-conclusion, which then motivates definitions and formal research (e.g. $\sum 2^n = -1$ is first "proved" using $\frac{1}{1-r}$ with $r=2$ and only later made rigorous with 2-adics). Do you count the informal discussion/proof in "all of math"?
That's what the paragraph I linked to talks about; Lean can never really capture all of math, when "all of math" is taken to mean "what mathematicians do".

[Franz Huschenbeth]

Snir Broshi said:

I didn't mean which math, but rather which parts of the act of doing math. For example, some math is inherently informal, such as discussions where you make a bunch of informal arguments to reach a pseudo-conclusion, which then motivates definitions and formal research (e.g. $\sum 2^n = -1$ is first "proved" using $\frac{1}{1-r}$ with $r=2$ and only later made rigorous with 2-adics). Do you count the informal discussion/proof in "all of math"?
That's what the paragraph I linked to talks about; Lean can never really capture all of math, when "all of math" is taken to mean "what mathematicians do".

I meant all "interesting" symbolically formalized math.

Part of the mathematicians job is to also separate the interesting from the uninteresting or not? If I make a informal argument, which leads to the principle of explosion, then everything collapses to a single truth value. Then one would have to find a way, in which the informal arguments "make sense" aka formalize them in some other model or theory, or just discard them as uninteresting.

So in this sense I would say I care about mainly math, and not the act of math.

[Niels Voss]

At the very least, Lean can formalize string rewriting systems, and every reasonable axiomatic system I know can be described as a string rewriting system. So Lean can theoretically formalize everything that is formalizable (provided you consider proving "System S proves P" to be a reasonable substitute to proving P). And Lean is itself a string rewriting system (≈ a Turing Machine). So I think the set of things Lean can formalize is exactly the set of things which can be formalized in any other sufficiently powerful formal system. (I guess Lean can't formalize proofs which are over 2^64 bytes long, but let's ignore that).

I think a much more interesting question than "Can Lean formalize all mainstream math?" is "Can Lean formalize all mainstream math in a natural way?"

[Franz Huschenbeth]

Niels Voss said:

At the very least, Lean can formalize string rewriting systems, and every reasonable axiomatic system I know can be described as a string rewriting system. So Lean can theoretically formalize everything that is formalizable (provided you consider proving "System S proves P" to be a reasonable substitute to proving P). And Lean is itself a string rewriting system (≈ a Turing Machine). So I think the set of things Lean can formalize is exactly the set of things which can be formalized in any other sufficiently powerful formal system. (I guess Lean can't formalize proofs which are over 2^64 bytes long, but let's ignore that).

I think a much more interesting question than "Can Lean formalize all mainstream math?" is "Can Lean formalize all mainstream math in a natural way?"

Natural in the sense that it mirrors natural language math or what exactly is meant by that?

[Kevin Buzzard]

Natural in the same sense that it would be unnatural to write a modern complex computer game in assembly language, even though it would in theory be possible.