> > The main problem will be to provide means to express the results from > checking "small" numbers (performed with a computer): numbers up to about 4 > x 10^18 for the binary Goldbach conjecture resp. about 9 x 10^30 for the > ternary Goldbach conjecture. Maybe each of the results must be provided as > theorem, like ~ 6gbe , which would be quite a lot...
The proof of ~6gbe takes about 500 bytes in set.mm, so recording Goldbach partitions of all even numbers up to 4x10^18 will require at least 10^21 bytes, i.e. a zettabyte. For comparison, that is more or less on the same order of magnitude as the amount of data generated worldwide (see https://en.wikipedia.org/wiki/Zettabyte#Comparisons_for_scale). At this point AI would have a better chance trying to lower this bound to something more feasible :-) -- 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/2e121181-6739-4bbb-9c20-6404f1280caeo%40googlegroups.com.
