I think I have a better paper proof of "union of algebraic sets is algebraic", and I formalized it, unfortunately in Coq because I do not speak Lean (can only read it), here:https://gist.github.com/andrejbauer/4dd8fa975fc98c9cc48dfdc776abde23 …
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.
-
-
-
I can certainly follow the "paper proof" in algebraic.v. Thanks! Note that in contrast I wrote my "paper proof" within my Lean proof -- I think it is easier for learners to follow. I did my homework: LEM is used at (forall x y, P x or Q y) -> (forall x, P x) or (forall y, Q y)
- Još 1 odgovor
Novi razgovor -
Č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.