I wonder whether humans could have realistically finished it without AI by 2100.

I would bet no. Because the original proof is so distributed, with parts of it being very old, and with parts of it being, as a first attempt, not the most concise or lucid route to the result, we were rapidly approaching a world where the empirical knowledge of how/why the result holds was literally dying.

The article refers to its use of the "first-generation proof". It would seem this proof is too large to be truly known by one person, and the group of people who "collectively knew" it grew old and started to die. Since its original formulation, mathematicians began to compile, consolidate, and revise the proof into a 2nd generation digested form (estimated to be 5000 pages instead of tens of thousands). But that effort was still so monumental in its own right that a 3rd gen proof project began to digest the 2nd gen proof before the 2nd gen proof was even finished. I believe both the 2nd and 3rd gen projects are still ongoing.

It will be interesting to see how small the proof gets once we finish learning how to obtain these results "efficiently" with the benefit of hindsight.