The Xena Project

@XenaProject

Mathematicians learning Lean. . Kevin Buzzard. Imperial College London. Prove a theorem. Write a function. .

Vrijeme pridruživanja: svibanj 2019.

Tweetovi

Blokirali ste korisnika/cu @XenaProject

Jeste li sigurni da želite vidjeti te tweetove? Time nećete deblokirati korisnika/cu @XenaProject

  1. Prikvačeni tweet
    13. sij

    I'm teaching algebraic geometry this term. Today is lecture one and I'm going to talk about why the union of two algebraic sets is an algebraic set. I'm formalising the proof in ! My Lean repository is hosted on github at

    Poništi
  2. 28. sij

    Highlights include LYM inequality and Kruskal-Katona (which takes me back to when I was a Part III student...)

    Prikaži ovu nit
    Poništi
  3. 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.

    Prikaži ovu nit
    Poništi
  4. 25. sij
    Poništi
  5. 22. sij

    In my alg geom course I prove V(I(V(S)))=V(S), for S a subset of k[X_1,X_2,...,X_n] and V and I the usual functions in the theory of affine alg varieties. I abstracted it and turned it into a new Lean maths challenge

    Poništi
  6. 22. sij

    But this might be the only finite model (modules over e.g. the rationals). So: closed under all products. I guess that "forall x, x = e" is allowed? So there are theories for which all models have size 1? I am not an expert here ;-)

    Poništi
  7. 18. sij
    Prikaži ovu nit
    Poništi
  8. 17. sij

    The reason it can't be the Nullstellensatz is that we didn't import any ring theory at all ;-)

    Prikaži ovu nit
    Poništi
  9. 17. sij

    alg geom lecture 3. We didn't prove the Nullstellensatz, but we proved something which looked very much like it:

    Prikaži ovu nit
    Poništi
  10. 16. sij

    While the code spends 10+ seconds compiling if you're viewing it in a browser, you can just read the extensive comments at the top.

    Prikaži ovu nit
    Poništi
  11. 16. sij

    OK lecture 2 is about V, the map from subsets of k[X_1,...,X_n] to subsets of k^n. Formalisation went *much* better than lecture 1: I didn't even assume k was a field ;-) the doc is like a Rosetta Stone for students wanting to learn Lean.

    Prikaži ovu nit
    Poništi
  12. 14. sij

    Got Monday's lecture running in online Lean at this URL: . Ridiculously slow -- takes 30 seconds or more to compile (going from "Lean is busy" to "Lean is ready") :-/ Working on it.

    Poništi
  13. 14. sij
    Poništi
  14. 14. sij
    Poništi
  15. 14. sij

    New Lean maths challenge at : prove (ghk^{-1})^{-1}=kh^{-1}g^{-1} in a group.

    Poništi
  16. 13. sij

    So the union proof is finished but it is far too complex in places, and takes too long to compile. Perhaps issue #2 will help...

    Poništi
  17. 9. sij

    Evil dirty trick new Lean maths challenge (number 7) at . Is there a rational number whose reciprocal is zero? Moral: beware of computer science conventions.

    Poništi
  18. 28. pro 2019.
    Poništi
  19. 27. pro 2019.

    Can you prove that equivalence classes for an equivalence relation are non-empty in Lean? New Lean maths challenge at

    Poništi
  20. 23. pro 2019.

    New Lean maths challenge at : prove that the sum of the first n positive odd numbers is n^2.

    Poništi

Č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.

    Možda bi vam se svidjelo i ovo:

    ·