formalizing something of algebraic geometry

Stream: new members

[Hagb (Junyu Guo)]

Hi! My name is Junyu Guo (and my screen name is "Hagb"), a 4th semester undergraduate in Chongqing University, majoring in Information and Computing Sciences.
I have finished the tutorials and (maybe roughly) read Theorem Proving in Lean.
I am now learning algebraic geometry by reading the book Ideals, Varieties, and Algorithms, and trying to formalize something about Gröbner basis, variety and (maybe) elimination theory from this book (chapter 1, 2, 3).

[Hagb (Junyu Guo)]

I have formalized two simple lemmas, but took a long time and wrote long proofs.

[Kevin Buzzard]

Do all of the files you import have that thing at the beginning saying "this file has been ported to mathlib4"? If so then it is probably recommend that you read Theorem Proving in Lean 4 and upgrade to Lean 4. Lean 3 will be dead in a few months.

[Hagb (Junyu Guo)]

Kevin Buzzard said:

Do all of the files you import have that thing at the beginning saying "this file has been ported to mathlib4"? If so then it is probably recommend that you read Theorem Proving in Lean 4 and upgrade to Lean 4. Lean 3 will be dead in a few months.

Yes. All of them have been synchronized with mathlib4.

[Kevin Buzzard]

Lean 4 is very similar to Lean 3, except that whitespace now has meaning in tactic mode and some definitions have got capital letters in.

[Hagb (Junyu Guo)]

@Kevin Buzzard Thanks for the information! Then I am going to learn and switch to Lean 4.