Tweets
- Tweets, current page.
- Tweets & replies
- Media
You blocked @XenaProject
Are you sure you want to view these Tweets? Viewing Tweets won't unblock @XenaProject
-
Pinned Tweet
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
#Leanprover ! My Lean repository is hosted on github at https://github.com/ImperialCollegeLondon/M4P33 …@ImperialMathsThanks. Twitter will use this to make your timeline better. UndoUndo -
Highlights include LYM inequality and Kruskal-Katona (which takes me back to when I was a Part III student...)
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo -
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.Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo -
woo-hoo, done the first problem sheet question for my course using
#leanprover : https://github.com/ImperialCollegeLondon/M4P33/blob/01b3d6985742c3dc6c28dc1f847fb704ddd9f5a1/problem_sheets/sheet_1/question_1.lean#L16 …Thanks. Twitter will use this to make your timeline better. UndoUndo -
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 http://tinyurl.com/LeanMathsChallenges …
#leanproverThanks. Twitter will use this to make your timeline better. UndoUndo -
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 ;-)
Thanks. Twitter will use this to make your timeline better. UndoUndo -
Permalink which will always work: https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2FImperialCollegeLondon%2FM4P33%2Ff427bb3057138dc9ca52830f3147d3cec443a85a%2Fsrc%2Faffine_algebraic_set%2FV.lean … (the link in the first tweet is broken now because I added some non-mathlib imports)
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo -
The reason it can't be the Nullstellensatz is that we didn't import any ring theory at all ;-)
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo -
alg geom lecture 3. We didn't prove the Nullstellensatz, but we proved something which looked very much like it: https://github.com/ImperialCollegeLondon/M4P33/blob/020023f2d998d3de43aabc3214b8e5e78b9006a1/src/abstract_V_and_I.lean#L152 …
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo -
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 threadThanks. Twitter will use this to make your timeline better. UndoUndo -
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: https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2FImperialCollegeLondon%2FM4P33%2Fmaster%2Fsrc%2Faffine_algebraic_set%2FV.lean … I didn't even assume k was a field ;-)
@johncarlosbaez the doc is like a Rosetta Stone for students wanting to learn Lean.Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo -
Got Monday's lecture running in online Lean at this URL: https://tinyurl.com/alg-geom-union . Ridiculously slow -- takes 30 seconds or more to compile (going from "Lean is busy" to "Lean is ready") :-/ Working on it.
Thanks. Twitter will use this to make your timeline better. UndoUndo -
There is currently a point in https://github.com/ImperialCollegeLondon/M4P33/blob/master/src/affine_algebraic_set/union.lean … where mathematicians lose track. Why is this? Very vague thoughts athttps://xenaproject.wordpress.com/2020/01/14/my-algebraic-geometry-course/ …
Thanks. Twitter will use this to make your timeline better. UndoUndo -
Thoughts on Lean Together 2020:https://xenaproject.wordpress.com/2020/01/14/lean-together-2020/ …
Thanks. Twitter will use this to make your timeline better. UndoUndo -
New Lean maths challenge at http://tinyurl.com/LeanMathsChallenges … : prove (ghk^{-1})^{-1}=kh^{-1}g^{-1} in a group.
Thanks. Twitter will use this to make your timeline better. UndoUndo -
So the union proof is finished https://github.com/ImperialCollegeLondon/M4P33/blob/master/src/affine_algebraic_set/union.lean … but it is far too complex in places, and takes too long to compile. Perhaps issue #2 will help...
Thanks. Twitter will use this to make your timeline better. UndoUndo -
Evil dirty trick new Lean maths challenge (number 7) at http://tinyurl.com/LeanMathsChallenges … . Is there a rational number whose reciprocal is zero? Moral: beware of computer science conventions.
Thanks. Twitter will use this to make your timeline better. UndoUndo -
Everyone's doing it now ;-) (well,
@pruvisto is...)https://twitter.com/isaprover/status/1210910782440919040 …Thanks. Twitter will use this to make your timeline better. UndoUndo -
Can you prove that equivalence classes for an equivalence relation are non-empty in Lean? New Lean maths challenge at http://tinyurl.com/LeanMathsChallenges …
#leanproverThanks. Twitter will use this to make your timeline better. UndoUndo -
New Lean maths challenge at http://tinyurl.com/LeanMathsChallenges … : prove that the sum of the first n positive odd numbers is n^2.
Thanks. Twitter will use this to make your timeline better. UndoUndo
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.