@tao pre-compiled tables are rather common in implementations of numerical methods, such as e.g. computing the Г - function. It's remarkable that it's essentially the same trick helps in formal proofs.