Cambridge maths PhD student Bhavik Mehta has formalised around 1/3 of the Part III (MSc) combinatorics course https://www.b-mehta.co.uk/iii/mich/combinatorics.pdf … in #leanprover . Thorough write-up at https://b-mehta.github.io/combinatorics/ . Finite sets are tricky, but this is evidence that the API is now there in Lean.
-
Prikaži ovu nit
Highlights include LYM inequality and Kruskal-Katona (which takes me back to when I was a Part III student...)
01:54 - 28. sij 2020.
0 replies
0 proslijeđenih tweetova
1 korisnik označava da mu se sviđa
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.