Is there a book like Russell's Principia Mathematica but for modern day mathematics?

• mathlib

  36 1,625 8.8 Lean

  Lean 3's obsolete mathematical components library: please use mathlib4

  

As such, if you want some body of work similar to PM, the spiritual successor of that effort is formal proof libraries, such as metamath or Lean. You won't find this stuff in any printed book, because the nature of software verified proofs is that they're supposed to be checked and verified digitally by computer.

• lean-liquid

  3 154 4.1 Lean

  💧 Liquid Tensor Experiment

  

Re your second para: you make speculations, but here are the facts. There certainly is a bunch of interest right now in formalising mathematics, there are fully paid-up mathematicians like myself hanging out on the Lean chat, working on stuff like this -- undergraduates, PhD students, post-docs and permanent staff. The repo is here and it's coming along nicely. Movement is happening. But it will be a while before we can convince the "generic mathematician" that these tools are useful. The Scholze project linked to in those links above is just another data point, but I fear we will need many more.

• InfluxDB

  www.influxdata.com sponsored

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• natural_number_game

  1 290 2.8 Lean

  Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

  

I assume we're talking about the natural number game. I can't make fancy drop-down menus. I just wrote the Lean code, which is all available on github. Mohammad made the web interface. If you want to make a more powerful interface please feel free! I am not a computer scientist and I don't know anything about web design.

Suggest a related project