Kevin Buzzard, a mathematician at Imperial College London, writes about formalizing math in the Lean proof assistant and teaching it.
Commenters recommend his Natural Number Game as an enjoyable way to learn proofs step by step using Lean.
That's a truly fantastic recommendation.
Other thoughts:
* The "Exploding Dots" project came up with a creative way to present place value that leads into a lot of other concepts like number bases, algebraic structures, polynomials, and other things. (It's actually like a generalization of the abacus, with fun computer animation.) I'm not sure which presentation of this is best -- I think the original inventor has gone through like three different versions and there are several versions available online now.
* I'm a huge fan of the late math journalist Martin Gardner, who wrote a lot of really entertaining stuff about math as well as puzzles and games. His books are really brilliant and cover a very wide territory. On the other hand, they were mostly written for adult audiences (originally, mainly readers of Gardner's Scientific American column) and may contain cultural references that kids wouldn't get, not least because some of them go back to the 1960s. :-( Also in some cases there have been further discoveries in the decades since the columns were published, so learning about them only from Gardner's old work may not give a good sense of where things have gone since then (e.g., he famously originally introduced both the Game of Life and the RSA algorithm to mass audiences, which then learned a lot about both topics in the ensuing decades). But maybe have a peek because they do stress the "math is fun and you can do it for fun" and also "math is all kinds of stuff and…
The kernel of a proof assistant is one of the most important components because it represents the foundation of reasoning in that logical system. There's a lot of introductory literature now, such as [0][1][2][3].
> What kind of axiomatic basis is being used in ACL2 and similar systems?
ACL2 uses first-order logic and term rewriting, but this significantly hinders proof automation (done by ad-hoc searches).
> Or do the different systems have significant differences with how and what they can prove?
Yes. First-order logic can only quantify over individual elements of a set, second-order logic can quantify over sets, and so on. Higher-order logic is the foundation of assistants like Isabele/HOL light, which let you use classical reasoning.
Alternatively (and better from an engineering standpoint) are assistants based on type theory, such as Agda, Coq and Lean. Their kernels are just type checkers, which are relatively small programs, so theorem proving in those systems is literally just functional programming with a fancy type system (though exactly how those proofs are constructed is a UX choice).
> Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible?
Yes, in Coq you can print out the axioms (on top of the type system) that a result depends on. See [4] for information on Coq's logic and what axioms you can safely add (they are necessary for certain areas of math).
[0] (Coq)…
Not really adjacent to what we do today.
I view A.I. as dual to "neoliberal M.B.A. culture". Just as the business schools taught that managers should be generalists without craft knowledge applying coarse microeconomics, A.I. that we have created is the ultimate pliant worker that also knows nothing deep and works from statistics. In a bussiness ecosystem where analytics and presentations are more important than doing things, they are a perfect match. Of course, a bunches of statistician-firms chasing each other in circles is going to exhibit the folly, not wisdom, of crowds.
I think solution is to face reality that more people need to learn programming, and more domain knowledge needs to be codified old school. https://www.ma.imperial.ac.uk/~buzzard/xena/ I thus think is perhaps the best application of computing, ever.
Training A.I. to be a theorem prover tactic is a great way to make it better: if we can't do theory and empiricism at the same time, we can at least do meta-empiracism on theory building!
I think once we've codified all the domains like that and been running A.I. on the theories, we'll be better positioned to go back to the general A.I. problem, but we might also decided the "manually programmed fully automated society" is easier to understand and steer, and thus less alienation, and we won't even want general A.I.
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ :
> In this game, you get own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms).
Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance)
If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.
The website mentions some good courses, personally I love Richard Borcherds' YouTube channel[1] for both undergraduate and graduate courses. No frills, exceptionally clear, (mostly) bite-sized lectures that cover a good range of material (especially in geometry).
Something that might interest HN's demographic is Kevin Buzzard's Xena Project[2], centered around proof systems (in Lean). The natural numbers game [3] is particularly fun IMHO. I don't know if it counts as learning materials per se but it's certainly instructive.
[1] https://www.youtube.com/channel/UCIyDqfi_cbkp-RU20aBF-MQ/playlists
[2] https://xenaproject.wordpress.com/
[3] https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
I'd say TLA+ is designed more for software people trying to design systems, write down specs, and reason about how the thing behaves dynamically.
Lean is used mostly for writing down math proofs, and a lot less for software (although by the Curry–Howard correspondence, math proofs and programs have an equivalence, so the line is a little blurry). Lean has "mathlib", which is like a standard library of formally verified math that people can contribute to and use in new proofs.
A big multi-year effort to start formalizing the proof of Fermat's Last Theorem in Lean 4 was approved recently: https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_FLT_talk.pdf