A Lean place · Random Matrix Theory
RMTLib
A Lean place for Random Matrix Theory results.
RMTLib is a Lean place for Random Matrix Theory results: a library where statements and proofs about random matrices are written in Lean and checked by computer.
Random matrix theory connects with number theory, notably through the statistics of zeros of the Riemann zeta function, whose functional equation Tate's thesis recovers from local factors at every place. A library is a place in its own right: a setting where results are worked out in precise local terms and then shared. The link to RMTLib will be published here when available.