On Thu, 13 Feb 2020 19:33:14 -0800 (PST), Norman Megill <[email protected]> wrote: > I worked out an estimate (in hours) for jobs 133-160 based on the theory > that the time to save a compressed proof is proportional to the run time of > 'minimize'. ... > job160.cmd: mideulem 404.4
That's less than 17 days, or only about 2 1/2 weeks. No big deal. I've had other (non-metamath) process executions take longer. Computer time is *way* cheaper than human time. That said, if we could reasonably break up that proof into smaller components instead of its current 334 steps, it would probably be easier to *understand* --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1j2crr-0001Mg-Tj%40rmmprod07.runbox.
