Tweetovi
- Tweetovi, trenutna stranica.
- Tweetovi i odgovori
- Medijski sadržaj
Blokirali ste korisnika/cu @XenaProject
Jeste li sigurni da želite vidjeti te tweetove? Time nećete deblokirati korisnika/cu @XenaProject
-
Prikvačeni 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 …@ImperialMathsHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Highlights include LYM inequality and Kruskal-Katona (which takes me back to when I was a Part III student...)
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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 nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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 …Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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 …
#leanproverHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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 ;-)
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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)
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
The reason it can't be the Nullstellensatz is that we didn't import any ring theory at all ;-)
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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 …
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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 nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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.Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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/ …
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Thoughts on Lean Together 2020:https://xenaproject.wordpress.com/2020/01/14/lean-together-2020/ …
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
New Lean maths challenge at http://tinyurl.com/LeanMathsChallenges … : prove (ghk^{-1})^{-1}=kh^{-1}g^{-1} in a group.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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...
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
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.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Everyone's doing it now ;-) (well,
@pruvisto is...)https://twitter.com/isaprover/status/1210910782440919040 …Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Can you prove that equivalence classes for an equivalence relation are non-empty in Lean? New Lean maths challenge at http://tinyurl.com/LeanMathsChallenges …
#leanproverHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
New Lean maths challenge at http://tinyurl.com/LeanMathsChallenges … : prove that the sum of the first n positive odd numbers is n^2.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoniš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.