Re:Palomar: A registry of Lean verified mathematics
by pfdietz on Wednesday August 19, 2026 @08:23AM
(#49360588)
Every math paper ever (there are about 4 million of them) will get formalized. One benefit of this is finding out which ones were actually correct, and which had unrecognized flaws in their claimed results.
After that, we can do statistics to see which ideas in math are most used, and perhaps mine for unrecognized patterns, refactoring math to find new abstractions.
My man Terrance Tao, I hope to contribute to your symphony of progress.
If the interrelationships of this are also exposed and searchable, if it can build many bridges inside itself, then this is truly the cipher key to all that can be known.