@tao@mathstodon.xyz In the old days logarithms were hard to calculate so people compiled them into large logarithm tables. Later we used tools like calculators in their place. I wonder if something similar is happening with proofs. They have been hard to generate so we store our efforts in publications. But as auto-proof and auto-write-up tools get more capable there will be less need to 'cache' them as a giant corpus. Instead people may simply run them on demand.