@tao

I have limited knowledge of lean, so I let claude read the original .tex source and let it make its own long term and short term plan, write them in todo files and its own memory files and so on.

The only thing I have interfered with are some design choices in the beginning about how to set up the indeterminates in the polynomial ring and their ordering (which determines the term ordering).