|
The Xena Project
@
XenaProject
London
|
|
Mathematicians learning Lean. xenaproject.wordpress.com. Kevin Buzzard. Imperial College London.
Prove a theorem. Write a function. #leanprover.
|
|
|
391
Tweetovi
|
80
Pratim
|
1.096
Osobe koje vas prate
|
| Tweetovi |
|
The Xena Project
@XenaProject
|
16 h |
|
Once we have taught computers to do maths for us, we'll have plenty of time on our hands to plot a revolution ;-)
|
||
|
|
||
|
The Xena Project
@XenaProject
|
1. velj |
|
It's currently hard to reproduce, but Jim Arthur is very happy to talk details about his proofs to any expert who is interested. The holes will probably, hopefully, be filled in the future.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
1. velj |
|
We should teach them all, because then we'll find out which ones work best in which areas. You should add a HoTT system to your list as well.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
31. sij |
|
@pruvisto @derKha I'm on the way to the Hausdorff center @HCM_Bonn for the #leanprover / ForTheL weekender :-) See you there!
|
||
|
|
||
|
The Xena Project
@XenaProject
|
30. sij |
|
Here's the question made into a level of a computer game:
leanprover-community.github.io/lean-web-edito…
|
||
|
|
||
|
The Xena Project
@XenaProject
|
30. sij |
|
Dumb question: my intuition (poor as it is!) says that if X is provable classically then not not X will always be provable constructively. Is this true?
|
||
|
|
||
|
The Xena Project
@XenaProject
|
29. sij |
|
The point is that you can prove the result even "without assuming that every statement is true or false"! You can prove it using constructive logic, without the law of the excluded middle. This is exactly what Chris' proof does and what mine doesn't do.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
28. sij |
|
It's not so much that I like classical logic, it's just that I don't understand any other kind! I don't know if P is true or false either -- that's why I checked all the cases ;-)
Actually, #leanprover taught me how to think constructively and I can check Chris' proof in Lean.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
28. sij |
|
It's true when P is true, and it's true when P is false, so it's true!
|
||
|
|
||
|
The Xena Project
@XenaProject
|
28. sij |
|
Highlights include LYM inequality and Kruskal-Katona (which takes me back to when I was a Part III student...)
|
||
|
|
||
|
The Xena Project
@XenaProject
|
28. sij |
|
Cambridge maths PhD student Bhavik Mehta has formalised around 1/3 of the Part III (MSc) combinatorics course b-mehta.co.uk/iii/mich/combi… in #leanprover . Thorough write-up at b-mehta.github.io/combinatorics/ . Finite sets are tricky, but this is evidence that the API is now there in Lean.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
28. sij |
|
Hi Michael, and thanks for your comments. I only had an hour, I couldn't say everything. I'm writing a longer piece where I will certainly mention Steingart -- many thanks for reminding me again about their work. Just re-read their classification paper.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
28. sij |
|
Agreed -- many thanks Barbara for putting this well-thought-out reply together. I had a one hour slot and couldn't say everything, but you make some very good points.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
27. sij |
|
I view mine as highly-constrained creativity followed by the essential step of making sure it's all correct. In some areas this can mean relying on work you can't check yourself but the elders say is OK. Both parts of the process are important to me.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
26. sij |
|
*Your* 285 page paper clearly contains a lot of perspiration! But it depends on missing claims of other people which add up to another 100 more, and which shouldn't be your problem. In Lean your main theorem would have an irritating orange line under it -- "not completely done".
|
||
|
|
||
|
The Xena Project
@XenaProject
|
26. sij |
|
Good question. I am not keeping pace because the Nullstellensatz is a bunch of commutative algebra which still isn't done in Lean and is done in the course. However the "pace" of the course wrt formalisation is very up and down. Working on formalising Zariski's Lemma right now.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
26. sij |
|
For the human sloppy/lazy problem I have no idea what to do, but am enjoying trolling mathematicians about the issue. On the computer side I have one idea -- if mathematicians *try to use these systems to do normal maths* then the systems will get better much more quickly.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
26. sij |
|
There are two different issues. Humans being sloppy/lazy (which has always been true but which I think is getting worse because of pressure to publish), and the observation that computers don't have that problem but instead have a whole bunch of other problems.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
25. sij |
|
I am simply pointing out that humankind has got into the habit of doing a poor job of the "perspiration" part of mathematics. You can't leave bits out and still say you're done. Of course it can all be completed, in theory. But not completing it might cause trouble down the line.
|
||
|
|
||
|
The Xena Project
@XenaProject
|
25. sij |
|
woo-hoo, done the first problem sheet question for my course using #leanprover : github.com/ImperialColleg…
|
||
|
|
||