Difficulty of formalizing Hartshorne's exercises

Stream: maths

[Roman Bars]

How difficult would it be to formalize the statements of the exercises in Hartshorne's textbook on algebraic geometry? What about the solutions?

[Johan Commelin]

Given the current state of the art, I think it would be very impressive to get past page 5.

[Kevin Buzzard]

I skipped chapter 1 and started with chapter 2 when I thought about this, but the first exercise was about a constant sheaf and we don't have those in mathlib yet. On the other hand Imperial students did some of the exercises about sheaves (e.g. gluing) within the context of top spaces.

[Kevin Buzzard]

Hartshorne's definition of presheaf is wrong as well, which makes things worse. for him it's not a functor, there is some random extra axiom F(0)=bot.

[Bhavik Mehta]

Johan Commelin said:

Given the current state of the art, I think it would be very impressive to get past page 5.

I don't know Hartshorne at all well, but is there anything you think would make it easier to do this?

[Johan Commelin]

A more extensive commutative algebra library