The Xena Project

@XenaProject

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

Joined May 2019

Tweets

You blocked @XenaProject

Are you sure you want to view these Tweets? Viewing Tweets won't unblock @XenaProject

  1. Pinned Tweet
    Jan 13

    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

    Undo
  2. Jan 28

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

    Show this thread
    Undo
  3. Jan 28

    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.

    Show this thread
    Undo
  4. Jan 25
    Undo
  5. Jan 21

    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

    Undo
  6. Jan 21

    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 ;-)

    Undo
  7. Jan 18
    Show this thread
    Undo
  8. Jan 17

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

    Show this thread
    Undo
  9. Jan 17

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

    Show this thread
    Undo
  10. Jan 15

    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.

    Show this thread
    Undo
  11. Jan 15

    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.

    Show this thread
    Undo
  12. Jan 14

    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.

    Undo
  13. Jan 14
    Undo
  14. Jan 14
    Undo
  15. Jan 14

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

    Undo
  16. Jan 13

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

    Undo
  17. Jan 9

    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.

    Undo
  18. 28 Dec 2019
    Undo
  19. 27 Dec 2019

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

    Undo
  20. 23 Dec 2019

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

    Undo

Loading seems to be taking a while.

Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.

    You may also like

    ·