Contributors to PROOF101

Introduction to Formal Verification & Proof Assistants (PROOF101) is the result of collaborative effort from many dedicated individuals. This page recognizes all who have contributed to making this course possible.

Course Leadership

Main Organizer

• Daniel Dia — Course creator, primary instructor & organizer (American University of Beirut); Computer & Communications Engineering (CCE) and Mathematics dual-degree student (AUB).

Faculty Mentors & Advisors

• Dr. Kinan Dak al Bab — Faculty mentor, Boston University | Website

  • Provided essential feedback and guidance throughout course development
  • Coordinated Dr. Robert Lewis’s guest lecture for Week 8
  • Ongoing support and mentorship

• Dr. Assaf Kfoury — Faculty advisor, Boston University | Website

  • Provided valuable support and feedback
  • Gave guest lecture for Week 7
  • Academic guidance and mentorship

Guest Lecturers

• Rida Hamadani (they/them) — Mathematical formalization researcher, former Lean Expert at Harmonic, Graduate student in resurgence theory (LMAP, France) | Website

  • Week 4: “Introduction to Tactic-based Proving” (Guest lecture)
  • Week 6: “Formalizing Mathematics and Contributing to Mathlib” (Guest lecture)
  • Offered to review Mathlib-related and CSlib-related mini-projects from course participants
  • Connected the course to the broader Lean mathematical community

• Dr. Assaf Kfoury — Professor of Computer Science (Boston University) | Website

  • Week 7: “The Mathematical Foundations of Proof Assistants” (Guest lecture)
  • Prepared a number of high-quality slides and handouts for course participants, covering: (1) the Church-Rosser property, (2) strong normalization of the simply-typed λ-calculus, (3) the Curry-Howard isomorphism, and (4) how these are part of the theoretical foundations of proof assistants (and Lean 4, in particular)

• Dr. Robert Lewis — Associate Teaching Professor of Computer Science (Brown University), coordinated by Dr. Kinan Dak al Bab | Website

  • Week 8: “Metaprogramming in Lean and Decision Procedures” (Guest lecture)

Organizational Partners

AUB Math Society

The AUB Math Society co-organized this course, providing essential support and helping bridge computer science and mathematics communities.

Key Contributors:

• Georges Sakr — Co-organization and logistics
• Mohammad Shouman — Co-organization and logistics
• Romy Kayrouz — Co-organization and logistics
• The entire AUB Math Society — For creating the infrastructure and community that made this course possible

Google Developer Groups on Campus @ AUB

The GDG on Campus @ AUB Software Team provided crucial organizational and logistical support, making this course possible as a student-led initiative.

Key Contributors:

• Lynn Hammoud — Co-organization and logistics
• Antonio Makhoul — Co-organization and logistics
• The entire GDG on Campus @ AUB club — For creating the infrastructure and community that made this course possible

Design & Visual Materials

• Alina Gurskaya — Graphic designer
  • Created the course logo
  • Helped design visual materials and branding

Course Materials

All course materials, unless explicitly specified (such as in the guest lectures), including slides, assignments, and course documentation, were developed by Daniel Dia with input and feedback from the above contributors.

Community Contributors

We also thank:

• All course participants who provide feedback and help improve the materials
• The Lean community for creating excellent documentation and tutorials
• The Mathlib contributors for building an incredible mathematical library

Key Contributors:

• Rida Hamadani
• Jad Abou Hawili

Contributing to PROOF101

Interested in contributing to PROOF101? We welcome:

• Bug reports and corrections in course materials
• Suggestions for improvements
• Additional examples and exercises
• Translations

Please reach out to Daniel Dia (dmd13@mail.aub.edu) regarding contributing to PROOF101.

License

Introduction to Formal Verification & Proof Assistants (PROOF101) by Daniel Dia and contributors is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International.

This list reflects contributions as of March 2026. If you believe you should be included or would like to update your information, please contact the course organizer.