Twitter | Pretraživanje | |
The Xena Project
Mathematicians learning Lean. . Kevin Buzzard. Imperial College London. Prove a theorem. Write a function. .
391
Tweetovi
80
Pratim
1.096
Osobe koje vas prate
Tweetovi
The Xena Project 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 ;-)
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 1. velj
Odgovor korisniku/ci @ejpatters @fairbanksjp
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 1. velj
Odgovor korisniku/ci @philipthrift @andrejbauer
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 31. sij
I'm on the way to the Hausdorff center for the / ForTheL weekender :-) See you there!
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 30. sij
Here's the question made into a level of a computer game:
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 30. sij
Odgovor korisniku/ci @EgbertRijke
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?
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 28. sij
Odgovor korisniku/ci @EgbertRijke @chrishughes244
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, taught me how to think constructively and I can check Chris' proof in Lean.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 28. sij
Odgovor korisniku/ci @EgbertRijke @chrishughes244
It's true when P is true, and it's true when P is false, so it's true!
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 28. sij
Odgovor korisniku/ci @XenaProject
Highlights include LYM inequality and Kruskal-Katona (which takes me back to when I was a Part III student...)
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 28. sij
Cambridge maths PhD student Bhavik Mehta has formalised around 1/3 of the Part III (MSc) combinatorics course in . Thorough write-up at . Finite sets are tricky, but this is evidence that the API is now there in Lean.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 28. sij
Odgovor korisniku/ci @MBarany @BarbaraFantechi i 3 ostali
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 28. sij
Odgovor korisniku/ci @HigherGeometer @BarbaraFantechi
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 27. sij
Odgovor korisniku/ci @HigherGeometer @pwr2dppl i 3 ostali
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 26. sij
Odgovor korisniku/ci @MathyPersiflage
*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".
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 26. sij
Odgovor korisniku/ci @HigherGeometer
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 26. sij
Odgovor korisniku/ci @MathyPersiflage
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 26. sij
Odgovor korisniku/ci @MathyPersiflage
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 25. sij
Odgovor korisniku/ci @MathyPersiflage
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.
Reply Retweet Označi sa "sviđa mi se"
The Xena Project 25. sij
woo-hoo, done the first problem sheet question for my course using :
Reply Retweet Označi sa "sviđa mi se"