Skip to main content
Proof Assistants Beta

Return to Answer

deleted 7 characters in body
Source Link
taylor.2317
taylor.2317
  • 1.3k
  • 8
  • 36

Lean

I am a professional mathematician with essentially nominimal experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Lean

I am a professional mathematician with essentially no experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Lean

I am a professional mathematician with minimal experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

add link to Lean learning resources
Source Link
edit approved Feb 9, 2022 at 21:08
Rob Lewis
edit approved Feb 9, 2022 at 21:08
Rob Lewis
  • 593
  • 6
  • 12

Lean

I am a professional mathematician with essentially no experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from;resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Lean

I am a professional mathematician with essentially no experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Lean

I am a professional mathematician with essentially no experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

add comment
Source Link
Kevin Buzzard
Kevin Buzzard
  • 2.6k
  • 12
  • 21

Lean

I am a professional mathematician with essentially no experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Lean

I am a professional mathematician with essentially no experience in coding or computer science, and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play.

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Lean

I am a professional mathematician with essentially no experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into the proof assistant community; ultimately I succeeded by attempting to formalise in Lean the statements and the proofs of the undergraduate example sheets in the introduction to proof course which I was teaching in the mathematics department at Imperial College London, and asking on the Lean chat when I got stuck. I am eternally indebted to Mario Carneiro for all the time he spent patiently dealing with my questions at that early stage; without him, I am pretty sure that I would not be using proof assistants now, I would just have given up. My header image on Twitter is a twisted and coloured-in version of part of the term created by my 100+ line tactic proof of the irrationality of $\sqrt{3}$ which was on the second example sheet, written when I still had no idea what I was doing. I could write a far shorter proof now, although now I don't need to, because the result is easily deducible from irrationality results in our wonderful mathematics library mathlib.

Since then, things have changed for mathematicians. Mohammed Pedramfar and myself wrote the Natural Number Game, a tutorial for mathematicians interested in learning Lean, which you can play on a computer through a web browser without having to install anything. Patrick Massot wrote a Lean tutorial project going through some basic results in undergraduate analysis, but here you have to install Lean 3 to play. If you want more, then the youtube playlist of talks from the 2020 conference "Lean for the curious mathematician" (LFTCM) is well worth a watch, and if you're reading this in early 2022 and want to participate in such a conference then applications are open right now for LFTCM 2022!

Going back to the original question then, Lean is extremely easy to install on linux (I installed it on a new laptop recently and it was just cutting and pasting one line of code and letting things happen by magic), and more of a bore to install on Windows but certainly not difficult. As for learning how to use it, if you have a mathematical background then Lean has a lot of resources for you to learn from; if you have a more computer-scientific background then Avigad et al's beautiful book Theorem Proving In Lean provides a great entry point. Either way, the Lean Zulip chat linked to above provides an efficient and polite and 24/7 helpline for questions of all levels; basic questions, for example, are welcome in the #new members stream.

Source Link
Kevin Buzzard
Kevin Buzzard
  • 2.6k
  • 12
  • 21