Palomar: A registry of Lean verified mathematics

(terrytao.wordpress.com)

30 points | by matt_d 2 hours ago ago

3 comments

  • seeknotfind 14 minutes ago

    Wow. This is incredible. Turning the entire field of mathematics into a formalized and connected system. An index of mathematical understanding. All fields will undergo this change!!!

    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.

  • tmshapland 31 minutes ago

    This is really cool! The thing I was looking for in the post is why people would contribute submissions to Palomar. What is the incentive?

    • mlpoknbji 18 minutes ago

      Same reason why you would use arxiv instead of posting the result to X.