← Ch 4 · Contents · ↑ Contents
Chapters: Ch 1 · Ch 2 · Ch 3 · Ch 4 · Ch 5
Mathematics in Computing & Applications
Formalizing a Proof in Lean Using Claude Code (YouTube, Watch History) Video demonstrating the workflow of using Claude Code to assist in developing formal proofs in Lean 4 — a dependent type theory-based proof assistant. Lean 4 is increasingly the tool of choice for mechanizing mathematical proofs; the Lean Mathlib library now contains tens of thousands of formalized results. This video sits at the intersection of pure mathematics, type theory, and AI-assisted development. [→ mathematics; formal-methods; scala-fp]
N N Taleb: Probability, Risk & the Ludic Fallacy (various, Watch History) Accumulated material from Taleb’s work on mathematical probability — his critique of using thin-tailed distributions (Gaussian, Poisson) to model fat-tailed phenomena (financial returns, pandemic casualties, war deaths). The mathematical core: kurtosis, L-moments, and why the law of large numbers converges far more slowly than classical statistics assumes. [→ mathematics; probability; risk]
Computational Number Theory & Cryptography Resources connecting pure number theory (prime factorization, elliptic curves, modular arithmetic) to modern cryptography — RSA, elliptic curve Diffie-Hellman, and post-quantum lattice-based cryptography. The deep structural connection between abstract algebra and practical security is one of mathematics’ most remarkable applied successes. [→ mathematics; cryptography; algorithms]