Overview of PROOF100

Welcome to Foundations of Mathematical Reasoning & Computer Science (PROOF100)! This initiative by the AUB Math Society is a hands-on bootcamp in the skills that PROOF101 is built on: reading and writing rigorous proofs, reasoning by induction, thinking precisely about programs, and knowing what a computer can and cannot do.

PROOF100 is a standalone course. The material here is the foundation of every theory course in a computer science or mathematics degree. Though beware: PROOF100 is run by students, not faculty, and is intended as a primer rather than a replacement for a full Discrete Structures or Data Structures & Algorithms course. It is meant to give you a taste of the subject, not to cover it thoroughly. It is also the preparatory course for PROOF101 (Introduction to Formal Verification & Proof Assistants using Lean4), which runs the following Spring.

REGISTER HERE

Course Details:

  • Primary Instructor & Organizer: Daniel Dia (dmd13@mail.aub.edu)
  • Session Leaders: Kevin Abou Rousse, Ali Ibrahim, Ayman Kaçan, Georges Khater, Omar Sinno, Yara Sleem, Ali Zbeeb, Wissam El Daouk
  • Teaching Assistant: Jad Abou Hawili (jka15@mail.aub.edu)
  • Organization: AUB Math Society
  • Target Audience: First-year ECE, CCE, CSE, CS, Math, and other STEM majors — and motivated high school students
  • Duration: 9 Weeks (15 sessions, 1.5-2.0 hours each)
  • Term: Monday 21 September 2026 — Thursday 26 November 2026 (subject to change)
  • Format: Hybrid (in-person sessions, live streamed and recorded)
  • Assessment: Five problem sets, handed in on paper, plus a final exam
  • Prerequisites: None (yes, really)
  • Last Updated: August 30, 2026

Quick access to materials and important links:

S1 | S2 | S3 | S4 | S5 | S6 | S7 | S8 | S9 | S10 | S11 | S12 | S13 | S14 | S15

Problem Sets | Final Exam

Motivation: Why Foundations?

PROOF100 teaches you to write proofs. We start from what a proof is, build up through logic and inference rules to induction in all its forms, and then turn that machinery on programs: proving that a sorting algorithm is correct, that a data structure maintains its invariant, that an algorithm runs in the time you claim, … etc. Along the way we answer questions such as “why is p → q true when p is false?”, “what exactly is the induction hypothesis doing?”, “what does it mean for a problem to be hard?”, “is there anything a computer simply cannot do?”, and more!

Whether you are a CS or engineering student who wants their code to be right rather than only tested, or a high school student who wants to learn foundational material, this course is built for you.

A note on workload: PROOF100 assumes nothing and builds everything, but expect roughly 3-4 hours (give or take) of work a week outside sessions, i.e. the readings, practice problems, and the five problem sets.

Course Structure

Weekly rhythm:

  • Phase A (21 Sep - 29 Oct) — two sessions per week, Monday and Thursday. Twelve sessions in six weeks.
  • Phase B (2 Nov - 16 Nov) — one session per week, Mondays.
  • Final exam — Thursday 26 November.

Session times: Monday and Thursday, 17:30 (tentative; confirmed before Week 1). Sessions are recorded and posted within 48 hours.

Assessment at a glance: five short problem sets, each covering roughly three sessions, handed in on paper. Between them, every session carries practice problems that are not collected and not graded.

Syllabus

Part 1: Logic and Proof (Sessions 1-5)

Part 1 answers the question the rest of the course depends on: what is a proof, and how one should go about writing one that is actually correct.

S1: Why Our Code Breaks (and What a Proof Is)

Orientation & What Is a Proof? (Mon 21 Sep) — with Daniel Dia

Core Concepts:

  • Course mechanics: structure, the five problem sets, certification, and the academic integrity policy
  • Real-world software disasters: Ariane 5 ($370M, integer overflow), Therac-25 (race condition, patient deaths), and Heartbleed (buffer over-read) vulnerabilities
  • The limits of testing: finite inputs vs infinite possibilities, Dijkstra’s principle, and a live demo
  • Statements, hypotheses, conclusions; the anatomy of a proof
  • True vs provable
  • Basic set notation as vocabulary: ∈, ⊆, ∪, ∩, , ∅, and set-builder notation
  • What a well-written proof looks like on paper and its “marking criteria”

Practice & Further Study:

S2: Propositional Logic

Syntax, Semantics, and Truth Tables (Thu 24 Sep) — with Kevin Abou Rousse

Core Concepts:

  • Connectives (¬, ∧, ∨, →, ↔), precedence, and parenthesization
  • Syntax vs semantics: formulas as objects, valuations as meaning, and the ⊨ relation
  • Truth tables; tautology, contradiction, satisfiability, and validity
  • Logical equivalences: De Morgan, distribution, contraposition, and p → q ≡ ¬p ∨ q
  • Overview of common truth tables
  • Normal forms (CNF/DNF); SAT stated as a problem

Practice & Further Study:

S3: Rules of Inference & Natural Deduction

Derivation Trees and the Machinery of Proofs (Mon 28 Sep) — with Ayman Kaçan

Core Concepts:

  • Proof systems as syntactic games: ⊢ versus ⊨
  • Inference rule notation: premises, conclusion, and side conditions
  • Introduction and elimination rules for every connective (∧I/∧E, ∨I/∨E, →I/→E, ¬I/¬E, ⊥E)
  • Derivation trees, built bottom-up and top-down
  • Hypothetical reasoning and discharging assumptions
  • Backward vs forward reasoning, with the same theorem proved both ways
  • Soundness and completeness

Practice & Further Study:

S4: Predicate Logic — Quantifiers, Binding, Scope

∀, ∃, and the Variables They Capture (Thu 1 Oct) — with Ayman Kaçan

Core Concepts:

  • Predicates, domains, ∀ and ∃; ∀I/∀E and ∃I/∃E as inference rules
  • Free and bound variables; the scope of a binder
  • α-renaming: why ∀x. P(x) and ∀y. P(y) are the same statement
  • Variable capture and failed substitution
  • Nested quantifiers and order sensitivity (∀ε∃δ vs ∃δ∀ε)
  • Negating quantified statements: ¬∀ ≡ ∃¬
  • Translating English into logic, and the ambiguity of English

Practice & Further Study:

S5: Proof Techniques

Writing Correct and Readable Proofs (Mon 5 Oct) — with Omar Sinno

Core Concepts:

  • Direct proof; contraposition; proof by contradiction
  • Proof by cases and exhaustion; biconditionals; uniqueness; counterexamples
  • Existence proofs: constructive vs non-constructive
  • Writing mathematical prose: what “let”, “suppose”, “consider”, “it suffices to show”, “WLOG” and others mean
  • Common mistakes: assuming the conclusion, division by zero, unjustified WLOG, etc.
  • Locating the defects in a flawed proof for practice

Practice & Further Study:

Part 2: Structures and Induction (Sessions 6-9)

Part 2 builds the objects that mathematics and programming both run on, i.e. sets, relations, functions, and then introduces ordinary and strong induction from Peano’s axioms, as well as structural and well-founded induction.

S6: Sets, Relations, Orders, Closures

Structure on Sets (Thu 8 Oct) — with Omar Sinno

Core Concepts:

  • Operations on sets, power sets, Cartesian products, and indexed families
  • Proving set identities as ∀-proofs
  • Relations as subsets of A × B; compositions and inverses
  • Properties: symmetry, antisymmetry, transitivity, and reflexivity
  • Equivalence relations, partitions, and quotients
  • Partial and total orders; Hasse diagrams
  • Closures: reflexive, transitive, and the reflexive-transitive closure R*, defined in three ways (smallest relation with the property; union of powers; inductively, by rules)
  • Russell’s paradox

Practice & Further Study:

S7: Functions, Cardinality & Diagonalization

Injections, Bijections, and Infinities of Different Sizes (Mon 12 Oct) — with Ali Ibrahim

Core Concepts:

  • Functions as relations; domains, codomains, and images
  • Injectivity, surjectivity, and bijectivity (with proofs in both directions)
  • Composition; inverses; left and right inverses and their relationship to injectivity and surjectivity
  • Function spaces B^A; functions as first-class objects
  • Countability (with proofs): ℕ, ℤ, and ℚ
  • Cantor’s diagonalization argument (i.e. ℝ is uncountably infinite); |P(A)| > |A|

Practice & Further Study:

  • Book of Proof (Hammack), Ch. 12, 13, 14
  • Practice: prove f is injective iff it has a left inverse (nonempty domain); write out both directions of the currying bijection and verify they are mutually inverse; prove there is no surjection A → P(A)

S8: Induction I — Naturals and Strong Induction

The Induction Principle and Where It Comes From (Thu 15 Oct) — with Yara Sleem

Core Concepts:

  • The induction principle stated as an inference rule
  • Why it is valid: the well-ordering of ℕ (detailed)
  • Peano axioms: zero, successor function, and induction
  • Ordinary induction (with attention to where the induction hypothesis is used)
  • Strong induction (and when the ordinary IH is insufficient)
  • Choosing what to induct on (with examples)
  • Classic failures and anecdotes: the “all horses are the same colour” proof
  • Course convention: every induction proof states the induction hypothesis explicitly (on its own line)

Practice & Further Study:

S9: Induction II — Structural and Well-Founded Induction

Inductive Definitions and the Induction Principles They Generate (Tue 20 Oct) — with Yara Sleem

Core Concepts:

  • Inductively defined sets, given by inference rules: base constructors and step constructors
  • Defining List, Tree, and ℕ inductively
  • Structural recursion: defining functions by cases on constructors
  • Structural induction: deriving the induction principle from the constructors
  • Rule induction over an inductively defined relation
  • Well-founded induction and termination: measures, decreasing arguments, and why while is harder than for
  • Functions that terminate but not structurally (gcd, Ackermann)

Practice & Further Study:

Part 3: Programs, Structures and Computational Complexity (Sessions 10-14)

Part 3 applies what we built up so far to programs: data structures and their invariants, asymptotic cost, recurrences, and programming paradigms.

S10: Recursion, Iteration & Data Structures I

The Call Stack, Invariants, and Linear Structures (Thu 22 Oct) — with Georges Khater

Core Concepts:

  • Recursive vs iterative formulations of the same algorithm, and translating between them
  • The call stack: stack frames, what recursion costs, and stack overflow
  • Tail recursion and accumulator passing
  • Memory model: the stack vs the heap, references, and pointers
  • Arrays vs linked lists
  • Stacks and queues: interface, implementation, and applications
  • Invariants: what one is, how to state it, and how to prove it is maintained
  • Loop invariants: initialization, maintenance, and termination

Practice & Further Study:

  • CLRS, Ch. 2, 10
  • Practice: convert a recursive sum to tail-recursive form and prove the two agree by induction; state and prove the loop invariant for insertion sort; for a queue built from two stacks, state the invariant relating them and prove the amortized cost is O(1)

S11: Data Structures II — Trees, Heaps, Graphs

Representation Plus Invariant (Mon 26 Oct) — with Georges Khater

Core Concepts:

  • Binary trees: representation, height, traversals (pre/in/post-order), and traversals as folds
  • Binary search trees: the BST invariant stated as a proposition about all descendants; insert, search, and delete
  • Balance: why unbalanced BSTs degrade; AVL and red-black trees at the level of which invariant they maintain
  • Heaps: the heap property as an invariant; sift-up and sift-down; heapsort; priority queues
  • Graphs: adjacency lists vs matrices; BFS and DFS
  • Hash tables
  • Every data structure here as a representation plus an invariant

Practice & Further Study:

  • CLRS, Ch. 6, 12, 22
  • Practice: write the BST invariant as a formal predicate over trees and prove in-order traversal yields a sorted list; exhibit a tree satisfying “node ≥ children” at every node that is not a BST
  • Problem Set 3 due today — hand it in on paper at the start of the session

S12: Asymptotics — Big-O from the Definition

Proving and Disproving Bounds (Thu 29 Oct) — with Ali Zbeeb

Core Concepts:

  • O, Ω, Θ, o, and ω, written out as quantifier statements (∃c, ∃n₀, ∀n ≥ n₀, …)
  • Proving f = O(g) by exhibiting c and n₀
  • Disproving a bound by negating the definition
  • Common growth classes and their ordering
  • Sums and series as an asymptotics tool: arithmetic, geometric, and harmonic; ∑ 1/i = Θ(log n)
  • Time vs space complexity; worst-case, average-case, and amortized costs
  • Why f = O(g) is considered abuse of notation

Practice & Further Study:

  • CLRS, Ch. 3
  • Mathematics for Computer Science, Ch. 9
  • Practice: prove 3n² + 5n + 2 = Θ(n²) from the definition with explicit constants; disprove 2^(2n) = O(2ⁿ) by negating the definition; rank eleven functions by growth rate with a justification for each adjacent pair
  • Problem Set 4 released today — due on paper at the start of S14 (Mon 9 Nov)

S13: Recurrences, Master Theorem & Divide-and-Conquer

Solving for the Cost of Recursion (Mon 2 Nov) — with Ali Zbeeb

Core Concepts:

  • Setting up a recurrence from an algorithm
  • Solving recurrences by “unrolling” and by recursion trees
  • Substitution method: guess, then prove by induction
  • Master’s Theorem: statement, the three cases, worked applications, and a case where it does not apply
  • Divide and conquer: mergesort, binary search, and Karatsuba
  • Worked case study: proving mergesort correct by strong induction, both that the output is sorted and that it is a permutation of the input

Practice & Further Study:

  • CLRS, Ch. 2, 4
  • Practice: solve T(n) = 2T(n/2) + n by unrolling, by recursion tree, and by the Master Theorem; produce a recurrence the Master Theorem cannot solve and identify which hypothesis fails

S14: Programming Paradigms & Functional Programming

Imperative, Object-Oriented and Functional Programming (Mon 9 Nov) — with Daniel Dia

Core Concepts:

  • Historical exposition (1936-2005): λ-calculus vs Turing machines, the software crisis, structured programming, OOP, Hoare’s null reference (1965), and the concurrency wall (2005)
  • Imperative paradigm: state, mutation, sequencing
  • OOP paradigm: encapsulation, inheritance, dynamic dispatch
  • Functional paradigm: purity, referential transparency, absence of observable side effects
  • First-class and higher-order functions; map, filter, fold, and compose as building blocks
  • Fold as the universal list recursion: deriving map, filter, length, sum, and reverse from it
  • Monoids as the structure fold requires
  • Currying and partial application
  • A short demonstration of Lean4 syntax

Practice & Further Study:

Part 4: The Limits of Computation (Session 15)

S15: Computability, Decidability & What Hardness Means

The Halting Problem, P vs NP, and the Limits of Computation (Mon 16 Nov) — with Wissam El Daouk

Core Concepts:

  • Computable functions: primitive recursion, composition, and the μ-operator; partial and general recursive functions (OLP 29)
  • A computable function that is not primitive recursive: Ackermann’s function (OLP 29.14)
  • Coding computations; the universal partial computable function, and why there is no universal total one (OLP 30.2-30.6)
  • The halting problem, by diagonalization (OLP 29.17, 30.7)
  • Computable vs computably enumerable sets (OLP 30.9-30.11)
  • Reductions; Rice’s theorem (OLP 30.15, 30.20)
  • Turing machines, their variants, and the Church-Turing thesis (OLP 31)
  • Universal Turing machines; the Entscheidungsproblem is unsolvable (OLP 32.3-32.8)
  • P and NP: verification vs solution, NP-completeness, SAT and Cook-Levin (Sipser Ch. 7)
  • What it means for a problem to be hard

Practice & Further Study:

  • The Open Logic Project, Ch. 29, 30, 31, 32
  • Introduction to the Theory of Computation (Sipser), Ch. 3 through 5, 7
  • Practice: prove the halting problem undecidable, writing out the diagonal construction in full; show “does this program ever print 7” is undecidable by reduction
  • Problem Set 5 due today — hand it in on paper at the start of the session

Final Exam

Thursday 26 November, 2 hours (tentative)

Closed book. Cumulative across S1-S15. Marks and certificates are issued before the December examination period begins.

Resources

Core Textbooks

All course textbooks are freely available online:

  1. Book of Proof — Richard Hammack

  2. Mathematics for Computer Science — Lehman, Leighton & Meyer (MIT 6.042)

Additional Course References

  1. Logic: Huth & Ryan, Logic in Computer Science (free) | The Open Logic Project (free)

  2. Algorithms: Cormen, Leiserson, Rivest & Stein (CLRS), Introduction to Algorithms (free)

  3. Computability: Sipser, Introduction to the Theory of Computation (Ch. 3-5, 7)

  4. Functional programming: Hughes, Why Functional Programming Matters (free) | Abelson & Sussman, SICP (free)

  5. Looking ahead: Pierce et al., Software Foundations: Logical Foundations (free) | Wadler, Propositions as Types (free)

Interactive Tools

Requirements & Policies

Problem Sets

There are five problem sets, each covering roughly three sessions. They are short by design: four to five problems each, released in one session and due at the start of a session about a week later.

#Problem SetReleasedDueCovers
1Logic and DeductionS3 · Mon 28 SepS5 · Mon 5 OctS1-S3
2Quantifiers, Proof Techniques, SetsS6 · Thu 8 OctS8 · Thu 15 OctS4-S6
3Functions and InductionS9 · Tue 20 OctS11 · Mon 26 OctS7-S9
4Data Structures and AsymptoticsS12 · Thu 29 OctS14 · Mon 9 NovS10-S12
5Recurrences and ParadigmsS14 · Mon 9 NovS15 · Mon 16 NovS13-S14

Computability (S15) is not covered by a problem set; it is examined on the final.

Submission is on paper, in person. Hand your work in at the start of the session on which it is due. If you cannot attend the session on which a problem set is due, arrange to submit it in advance by email. Work handed in after the session has begun is late.

PROOF100 maintains a strict zero-tolerance policy for academic dishonesty. Copying work, sharing solutions, or unacknowledged use of LLMs is prohibited and will result in zero credit and ineligibility for certification. Using an LLM to explain a concept is fine and encouraged; using one to generate a proof you then submit is not, whether or not you rewrite it in your own handwriting. Any use at all must be disclosed in a line at the top of your submission.

See the Problem Sets page for the full policy.

Attendance & Recordings

All sessions are recorded and posted within 48 hours. A motivated student can follow this course asynchronously, but problem sets are handed in on paper in person, and the board work in S5 cannot be replicated by watching.

Certification

Participation is open to all. Certification is reserved for those who demonstrate mastery.

Certificate of Distinction:

  • Attend at least 11 of 15 sessions
  • Submit at least 4 of the 5 problem sets
  • Score 75% or above on the final exam

Honors mention is awarded at the instructor’s discretion to the strongest performers in the cohort.

Note: depending on the student’s performance and personal circumstances, some requirements may be modified or dropped. This applies especially to our high school participants, whose schedules do not align with ours.

What Comes Next

PROOF100 graduates are the intended audience for PROOF101: Introduction to Formal Verification & Proof Assistants, running Spring 2027 with guest lecturers from Boston University, Brown University, LMAP, and AUB.

Acknowledgments

This course would not be possible without the people who volunteered their time to teach it.

Session Leaders:

  • Daniel Dia (CCE + Math) — S1: Orientation & What Is a Proof?; S14: Programming Paradigms & Functional Programming
  • Kevin Abou Rousse — S2: Propositional Logic
  • Ayman Kaçan — S3: Rules of Inference & Natural Deduction; S4: Predicate Logic, Quantifiers, Binding & Scope
  • Omar Sinno (ECE) — S5: Proof Techniques; S6: Sets, Relations, Orders & Closures
  • Ali Ibrahim (MECH + Math) — S7: Functions, Cardinality & Diagonalization
  • Yara Sleem (CSE + Math) — S8: Induction I — Naturals and Strong Induction; S9: Induction II — Structural and Well-Founded Induction
  • Georges Khater (CSE + Math) — S10: Recursion, Iteration & Data Structures I; S11: Data Structures II
  • Ali Zbeeb (CSE) — S12: Asymptotics — Big-O from the Definition; S13: Recurrences, Master Theorem & Divide-and-Conquer
  • Wissam El Daouk (CSE) — S15: Computability, Decidability & What Hardness Means

Organizational Support:

  • AUB Math Society — for organizing this initiative and providing essential support

And to all participants who bring energy, curiosity, and dedication to making this learning community thrive.

For a complete list of contributors to the course materials, see our PROOF100 “Contributors” page.

License

Foundations of Mathematical Reasoning & Computer Science (PROOF100) by Daniel Dia and contributors is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International.

This means you are free to:

  • Share — copy and redistribute the material in any medium or format
  • Adapt — remix, transform, and build upon the material

Under the following terms:

  • Attribution — You must give appropriate credit, provide a link to the license, and indicate if changes were made
  • NonCommercial — You may not use the material for commercial purposes
  • ShareAlike — If you remix, transform, or build upon the material, you must distribute your contributions under the same license

For the complete license text, visit: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode