Terence Tao on AI and Math, 2024

Terence Tao on AI and Math, 2024

really enjoyed listening to this one.

Terence Tao on latest of using machine to do math.

here's a randomish summary:

• he is using Lean.
• Lean now has a project called mathlib that tries to be a database of say college level maths. so to reduce tedium of proofs starting at axioms level.
• with computer help provers, now one can break a proof into many sub-parts, and each of the parts can be computer formally proved by others. thus, making it possible for larger team, say 20, to work on a computer proof.
• Machine learning is helpful. Example given is feeding it big data of knots of knot theory, and the varieties of their invariants, and have it try to figure how the relation to the knot's signature.
• latest, Large Language Model (e.g. chatgpt), is helpful in suggesting techniques, etc.

what Lean looks like

general summary