Ever wonder why software failures cause rockets to explode or medical devices to kill patients? From the $370 million Ariane 5 explosion (integer overflow) to the Therac-25 that killed six patients (race condition), catastrophic failures plague “correct-looking” code.

PROOF101 is a 10-week course (GDG @AUB × AUB Math Society) designed and delivered by Daniel Dia based on Brown's CS1715, in collaboration with Boston University faculty. Topics: dependent type theory, functional programming, tactics, semantics, Mathlib contributions, verified cryptography, metaprogramming, and Rust.

Testing can show bugs exist, never their absence. PROOF101 teaches you to mathematically prove your code is correct. Master Lean4, the proof assistant from Microsoft Research used to verify cryptography in Firefox and formalize Fields Medal-winning mathematics. Formal verification turns catastrophic runtime crashes into compile-time errors, eliminating entire classes of bugs before they cause harm.

Whether you’re a computer scientist wanting to write bulletproof code, a mathematician interested in mechanized proofs, or an engineer building safety-critical systems, this 10-week course equips you with tools for reasoning about programs with mathematical precision. Features include weekly interactive quizzes, hands-on programming assignments, and expert guest lectures from Rida Hamadani (LMAP, formerly Lean Expert at Harmonic), Dr. Rob Lewis (Brown University), Dr. Assaf Kfoury (Boston University), and more!

Prerequisites: Basic programming experience and familiarity with mathematical reasoning. No prior experience with functional programming or proof assistants required — we’ll build everything from first principles, starting with λ-calculus. Having completed CMPS211 (Discrete Structures) or EECE230 (Intro to Computation & Programming) is helpful but not required.

📘 For the full course schedule, materials, and detailed information, visit the course website:
https://danieldia-dev.github.io/proofs/