Section 1.8 Codes
Subsection 1.8.1 \(L\exists \forall N\)
LEAN is a proof assistant, which allows people to write the proof of theorems in a computer programme language. See the website of LEAN community.
A team of me, Huajian Xin, Ella Yu and others attempted to prove the prime number theorem on LEAN. See our Github repository. Ella Yu and I gave a talk about this project on a seminar of London Learning Lean held by Imperial College. Watch the recording here. See the slides here.
Subsection 1.8.2 Numerical Library of Mathematics Algorithm
I made a simple C++ library for numerical algorithms such as solving linear systems, integrals, differential equations and so on numerically. See my Github repository.
