Background needed for type theories, history and its use ...

Stream: new members

[Anh Nguyễn]

I joined the community for two months but have not really spent time to learn Lean and how it works. I find type theory is quite hard to follow and at this moment I am so confused about it. Could you please give me some information about what to study. And a brief timeline of type theories and how they are used in theorem prover

[Matteo Cipollina]

this is a good overview written by the creator of Coq:

https://plato.stanford.edu/entries/type-theory/

[Riccardo Brasca]

What are you goals? For example, if you are interested in formalizing calculus, linear algebra or similar stuff you can completely ignore type theory.

[Anh Nguyễn]

How did you start formalizing mathematics

Riccardo Brasca said:

What are you goals? For example, if you are interested in formalizing calculus, linear algebra or similar stuff you can completely ignore type theory.

[Riccardo Brasca]

You can try the natural number game, most of us started with it. Then you can choose any theorem and try to formalize it. Of course if you want to learn the foundations of Lean this is also possible, but it is quite different from formalizing a theorem.

[Riccardo Brasca]

It's like when you learn calculus you don't really need to know how real numbers are defined, and you need even less to know the axioms of mathematics.

[Anh Nguyễn]

Riccardo Brasca said:

You can try the natural number game, most of us started with it. Then you can choose any theorem and try to formalize it. Of course you want to learn the foundations of Lean this is also possible, but it is quite different from formalizing a theorem.

How much different is big formalizing projects from formalizing normal mathematics

[Anh Nguyễn]

Like FLT. They have to plan out how to do it before start?

[Anh Nguyễn]

Which kind of mathematics is harder to formalize and what are the strategies to formalize it

[Riccardo Brasca]

I don't completely understand the question, the difference is similar to proving (on paper) a small result compared to a big theorem, it's a lot more work. You can find the details on the strategy in the blueprint.

[Riccardo Brasca]

In particular yes, it's much better to have a very precise paper proof before starting the formalization process. This is true for big projects but also for small resutls.

[Anh Nguyễn]

FLT for regular primes is not done yet, right?

[Riccardo Brasca]

It's done.

[Anh Nguyễn]

I think there was a lot of work
How long it took to fully formalize it, and how many files, lines of code is it

[Riccardo Brasca]

You can have a look at the paper.

[Anh Nguyễn]

Thank you, I will take a look at it

[Anh Nguyễn]

How about Curry Howard correspondence

[Anh Nguyễn]

Matteo Cipollina said:

this is a good overview written by the creator of Coq:

https://plato.stanford.edu/entries/type-theory/

Type theory has been developed much and alter significantly compared to the one that was used in theorem provers in early days (Four Color Theorem verification)?

[Anh Nguyễn]

How much different it is from the early days to this day

[Niels Voss]

Type theory has been around much longer than the proof of the Four Color Theorem. There has been a lot of research in type theory within the past few years (think of things like Rust's type theory, Homotopy type theory, etc.), but the type theory used by Lean specifically is extremely similar to that used by Coq at the time of the Four Color Theorem.

[Niels Voss]

The two main learning resources for Lean are #mil, which is a learn-by-doing approach, and #tpil, which is a foundations-first approach. It sounds like you might be interested in #tpil. Are you interested in learning a lot about the metalogical aspects of type theory because you are interested in type theory specifically, or are just interested in learning how Lean actually works? If the latter, I recommend you start out with #tpil.

Learning the subject of type theory when you just want to use Lean is kind of like studying linguistics when you just want to learn a new language.

[Anh Nguyễn]

I want to know more about how Lean works and type theory. Formalizing mathematics is my secondary priority

[Anh Nguyễn]

In other words, I want to learn and understand how type theories (many different kinds) is served as the foundation of mathematics (I vaguely understand it, just knowing it is an alternative foundation replace set theory as way to avoid Russel Paradox).
Could you tell me the weakness and strength of each kind of type theory, and how it is implemented in the computer to construct mathematical objects in a way for computer to process

[Anh Nguyễn]

And about the relationship between computer science and mathematics

[Anh Nguyễn]

Those things are mentioned in many places but I want to truly understand it

[Niels Voss]

I'm not the person to ask about learning many different type theories, but even though #tpil only teaches you about one type theory, I still recommend it as a starting place for learning type theory because for some of the questions you have (like how the Curry-Howard correspondence works, and what's the relationship between CS and math) you only really need to know a single type theory. (Although of course its always insightful to learn more different type theories.)

[Niels Voss]

The point of type theory is not to avoid Russell's paradox. Modern set theories avoid Russell's paradox by either not having a set of all sets, or restricting the axiom schema of specification. Type theory does have some advantages over set theory, but avoiding Russell's paradox is not really the purpose of type theory.

[Anh Nguyễn]

Niels Voss said:

I'm not the person to ask about learning many different type theories, but even though #tpil only teaches you about one type theory, I still recommend it as a starting place for learning type theory because for some of the questions you have (like how the Curry-Howard correspondence works, and what's the relationship between CS and math) you only really need to know a single type theory. (Although of course its always insightful to learn more different type theories.)

I want to learn the type theory related to Lean first

[Anh Nguyễn]

And how earlier days theorem provers performed proving a statement

[Anh Nguyễn]

And some notable development in the field of automated theorem prover. Thank you so much

[Timothy Chow]

Type theory goes back to Russell, who was trying to develop the foundations of mathematics back in the days when a lot of things we take for granted nowadays were not so clear. Avoiding the paradoxes of set theory was not his only goal, but it was certainly something he had in mind. However, Russell's theory had a number of awkward features and has basically been abandoned.

Then Church came along and developed "simple type theory," based on the lambda-calculus. Simple type theory is still important today, and forms the basis for some proof assistants such as HOL Light. If you really want to understand type theory thoroughly, then mastering simple type theory is a pretty good way to start.

The type theory in Lean, however, is more complicated. To motivate it, the following slightly fictionalized historical account may be helpful. Early designers of programming languages soon found that the notion of a type (and here I use "type" in the sense of a programming language such as C) was very useful; in particular, it would allow the compiler to catch a lot of bugs via a type-checking algorithm. They developed rather sophisticated typing systems and associated type-checking algorithms, all in the service of developing good programming languages, and not the foundations of mathematics. But at some point, it dawned on people that there was an extremely close parallel between the typing rules and the rules of logic (or at least, intuitionistic logic). This parallel is what we now call the Curry-Howard correspondence. The informal phrasing that I like is:

Proof checking is isomorphic to type checking.

So if you want to develop a proof assistant, you can simply steal the type-checking code from the compiler of a strongly typed programming language. Okay, maybe that's an oversimplification, but it's not far from the truth. It explains why, in Lean, a colon is used both for assertions (the technical term is "judgments") of the form "n is a natural number" (n : N) and for assertions of the form "X is a proof of theorem T" (X : T). In both cases, we verify the assertion by invoking a type-checking algorithm.

If you have some background in axiomatic set theory, the type-theoretic practice of putting theorems and natural numbers (and other mathematical objects) on an equal footing takes some getting used to. The "traditional" approach defines a formal language by specifying the syntax, and then introducing mathematical structures as a semantic interpretation of the formal language. Proofs live in the syntactic world and mathematical structures live in the semantic world, and you have to be careful to keep the distinction clearly in mind. In type theory, or at least the kind of type theory used in Lean, proofs are on an equal footing with natural numbers and real numbers and other mathematical objects. In type theory, the rules for constructing complicated mathematical objects are therefore deeply intertwined with the rules of logic.

This has the consequence that if you really want to learn type theory, you can't quite go about it the usual way that you learn, say, number theory or differential geometry or whatever. It's more like learning axiomatic set theory; you need to absorb a system of rules for manipulating expressions. Asking "what is a type?" is akin to asking "what is a set?"; there's no snappy answer that is fully accurate, since an accurate answer must specify the entire system of rules.

As for where you can learn more details, I rather like the book "Program = Proof" by Samuel Mimram. Another good book is "Type Theory and Formal Proof: An Introduction," by Nederpelt and Geuvers.

One final comment. The Curry-Howard correspondence, which is a major motivation for modern type theory, gets a bit messy when you bring classical logic (the law of the excluded middle) into the picture. For this reason, many type-theoretic proof assistants have a strong constructive flavor. However, Lean, or at least mathlib, has embraced classical logic.

[Philippe Duchon]

As an additional note on the bibliography, Samuel Mimram's book (or at least a version of it) is available on his webpage, in the "Teaching" section (for the Computational Logic course).

[suhr]

Some bits of history a lot of people forget:

• In the first half of XX century, Brouwer–Heyting–Kolmogorov interpretation of logic was formulated
• Inspired by this interpretation, de Bruijn develops Automath (starting from 1967), the first proof assistant (proof checker really) based on dependent types

In parallel to that

• In 1967, Errett Bishop publishes Foundations of Constructive Analysis, a groundbreaking work in constructive mathematics
• In 1972, Martin-Löf publishes his dependent type theory, with intend to give a formal ground for Bishop style constructive mathematics. Note, that in https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf Martin-Löf calls types "sets"

So dependent type theory is a natural development of constructive mathematics.

[suhr]

Some history of Automath: https://alexandria.tue.nl/repository/freearticles/597627.pdf

History of constructivism in the 20th century: https://pure.uva.nl/ws/files/22817397/_Troelstra_A_S_History_of_Constructivism_in_the_2.pdf