The Weil conjectures formalized in Lean

Just to confirm:

Weil made a few conjetures. Someone else proved all the conjeture later. You formalized the statement of the conjetures and the proofs in Lean. (?)