Mixing
Which mathematical definitions should be formalised in Lean?
Clash Royale CLAN TAG#URR8PPP
up vote
8
down vote
favorite
The question.
Which mathematical objects would you like to see formally defined in version 3.4.1 of the Lean Theorem Prover?
Examples.
Topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and I heard earlier today that we might have modular forms. There is a sort of an indication of where we are.
What else should we be doing? What should we work on next?
Some background.
Over the last year I have become increasingly interested in the mathematics library for the Lean theorem prover, a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language.
My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. Let's get one thing straight -- formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.
But formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.
But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Tom Hales' formal abstracts project plans to formalise the statements of new theorems as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in Lean and send it to Tom Hales! If you need hints about how to do that, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.
We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.
big-list proof-assistants bourbaki lean-theorem-prover
edited 1 hour ago
Martin Sleziak
2,74432028
asked 1 hour ago
Kevin Buzzard
27.3k5107197
add a comment |Â
up vote
8
down vote
favorite
The question.
Which mathematical objects would you like to see formally defined in version 3.4.1 of the Lean Theorem Prover?
Examples.
Topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and I heard earlier today that we might have modular forms. There is a sort of an indication of where we are.
What else should we be doing? What should we work on next?
Some background.
Over the last year I have become increasingly interested in the mathematics library for the Lean theorem prover, a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language.
My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. Let's get one thing straight -- formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.
But formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.
But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Tom Hales' formal abstracts project plans to formalise the statements of new theorems as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in Lean and send it to Tom Hales! If you need hints about how to do that, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.
We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.
big-list proof-assistants bourbaki lean-theorem-prover
edited 1 hour ago
Martin Sleziak
2,74432028
asked 1 hour ago
Kevin Buzzard
27.3k5107197
1
Is there a mailing list or forum where all this is being discussed?
– David Roberts
1 hour ago
leanprover.zulipchat.com . Mailing list is very quiet, chat is much more lively.
– Kevin Buzzard
1 hour ago
add a comment |Â
up vote
8
down vote
favorite
up vote
8
down vote
favorite
The question.
Which mathematical objects would you like to see formally defined in version 3.4.1 of the Lean Theorem Prover?
Examples.
Topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and I heard earlier today that we might have modular forms. There is a sort of an indication of where we are.
What else should we be doing? What should we work on next?
Some background.
Over the last year I have become increasingly interested in the mathematics library for the Lean theorem prover, a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language.
My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. Let's get one thing straight -- formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.
But formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.
But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Tom Hales' formal abstracts project plans to formalise the statements of new theorems as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in Lean and send it to Tom Hales! If you need hints about how to do that, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.
We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.
big-list proof-assistants bourbaki lean-theorem-prover
edited 1 hour ago
Martin Sleziak
2,74432028
asked 1 hour ago
Kevin Buzzard
27.3k5107197
The question.
Which mathematical objects would you like to see formally defined in version 3.4.1 of the Lean Theorem Prover?
Examples.
Topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and I heard earlier today that we might have modular forms. There is a sort of an indication of where we are.
What else should we be doing? What should we work on next?
Some background.
Over the last year I have become increasingly interested in the mathematics library for the Lean theorem prover, a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language.
My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. Let's get one thing straight -- formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.
But formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.
But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Tom Hales' formal abstracts project plans to formalise the statements of new theorems as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in Lean and send it to Tom Hales! If you need hints about how to do that, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.
We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.
big-list proof-assistants bourbaki lean-theorem-prover
big-list proof-assistants bourbaki lean-theorem-prover
edited 1 hour ago
Martin Sleziak
2,74432028
asked 1 hour ago
Kevin Buzzard
27.3k5107197
edited 1 hour ago
Martin Sleziak
2,74432028
asked 1 hour ago
Kevin Buzzard
27.3k5107197
edited 1 hour ago
Martin Sleziak
2,74432028
edited 1 hour ago
Martin Sleziak
2,74432028
edited 1 hour ago
Martin Sleziak
2,74432028
2,74432028
asked 1 hour ago
Kevin Buzzard
27.3k5107197
asked 1 hour ago
Kevin Buzzard
27.3k5107197
asked 1 hour ago
Kevin Buzzard
27.3k5107197
27.3k5107197
1
Is there a mailing list or forum where all this is being discussed?
– David Roberts
1 hour ago
leanprover.zulipchat.com . Mailing list is very quiet, chat is much more lively.
– Kevin Buzzard
1 hour ago
add a comment |Â
1
Is there a mailing list or forum where all this is being discussed?
– David Roberts
1 hour ago
leanprover.zulipchat.com . Mailing list is very quiet, chat is much more lively.
– Kevin Buzzard
1 hour ago
1
1
Is there a mailing list or forum where all this is being discussed?
– David Roberts
1 hour ago
Is there a mailing list or forum where all this is being discussed?
– David Roberts
1 hour ago
leanprover.zulipchat.com . Mailing list is very quiet, chat is much more lively.
– Kevin Buzzard
1 hour ago
leanprover.zulipchat.com . Mailing list is very quiet, chat is much more lively.
– Kevin Buzzard
1 hour ago
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
4
down vote
I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the number field case.
I am currently unclear on whether there is a way to rigorously formalise the statement of the full Global Langlands Reciprocity Conjecture, or whether it is just supposed to be a "philosophy" which implies functoriality. I wish I understood more of Jim Arthur's paper on the subject.
answered 1 hour ago
Kevin Buzzard
27.3k5107197
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
4
down vote
I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the number field case.
I am currently unclear on whether there is a way to rigorously formalise the statement of the full Global Langlands Reciprocity Conjecture, or whether it is just supposed to be a "philosophy" which implies functoriality. I wish I understood more of Jim Arthur's paper on the subject.
answered 1 hour ago
Kevin Buzzard
27.3k5107197
add a comment |Â
up vote
4
down vote
I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the number field case.
I am currently unclear on whether there is a way to rigorously formalise the statement of the full Global Langlands Reciprocity Conjecture, or whether it is just supposed to be a "philosophy" which implies functoriality. I wish I understood more of Jim Arthur's paper on the subject.
answered 1 hour ago
Kevin Buzzard
27.3k5107197
add a comment |Â
up vote
4
down vote
up vote
4
down vote
I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the number field case.
I am currently unclear on whether there is a way to rigorously formalise the statement of the full Global Langlands Reciprocity Conjecture, or whether it is just supposed to be a "philosophy" which implies functoriality. I wish I understood more of Jim Arthur's paper on the subject.
answered 1 hour ago
Kevin Buzzard
27.3k5107197
I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the number field case.
I am currently unclear on whether there is a way to rigorously formalise the statement of the full Global Langlands Reciprocity Conjecture, or whether it is just supposed to be a "philosophy" which implies functoriality. I wish I understood more of Jim Arthur's paper on the subject.
answered 1 hour ago
Kevin Buzzard
27.3k5107197
answered 1 hour ago
Kevin Buzzard
27.3k5107197
answered 1 hour ago
Kevin Buzzard
27.3k5107197
answered 1 hour ago
Kevin Buzzard
27.3k5107197
27.3k5107197
add a comment |Â
add a comment |Â
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f311071%2fwhich-mathematical-definitions-should-be-formalised-in-lean%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
1
Is there a mailing list or forum where all this is being discussed?
– David Roberts
1 hour ago
leanprover.zulipchat.com . Mailing list is very quiet, chat is much more lively.
– Kevin Buzzard
1 hour ago