Our great sponsors
-
M40001_lean
Lean 3 material related to Imperial College's "Introduction to University Mathematics" course
-
InfluxDB
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.
Somewhat orthogonal, I think what Imperial College London is doing in their undergraduate introductory mathematics course -- teaching Lean to freshmen (who are interested) -- is highly interesting. It took me until my 3rd or 4th semester until I properly understood how to write a proof. Having taken a class on interactive theorem provers in my 4th semester definitely helped this. The fact that the computer immediately tells you that your proof is correct is really nice, and really helps you learn. Also, the computer showing you the current proof state and freeing you from juggling with all the assumptions in your head teaches you how to do this and shows you which operations on your assumptions are possible.