PROOF101 Programming Assignments

Overview

Throughout the course, you will complete 4 programming assignments that reinforce key concepts through hands-on Lean4 coding:

• “Programming” Assignment 1 — Getting started with Lean4 (not a “programming assignment” strictly speaking)
• Programming Assignment 2 — type theory and dependent types (Lean4)
• Programming Assignment 3 — functional programming (Lean4)
• Programming Assignment 5 — proof tactics and semantics (Lean4)

Each assignment contains multiple problems that build progressively from foundational concepts and simpler problems to more advanced applications. You’ll complete implementations by replacing sorry placeholders with working Lean4 code.

Example Problem

/- Problem 1.1 (5 points)
Implement `twice` - a function that takes a function and returns a new
function that applies it twice.
-/
def twice {α : Type} (f : α → α) : α → α :=
  sorry

-- Test cases
-- #eval (twice (· + 1)) 5          -- Should output: 7
-- #eval (twice (· * 3)) 2          -- Should output: 18

Assignment Requirements

When completing assignments, you must:

• Replace sorry with your implementation: each sorry marks code you need to write
• Ensure all definitions type-check: your code must compile without errors
• Test your code: uncomment #eval statements to test your code
• Do not modify type signatures: function types are provided and should not be changed
• Attempt bonus problems: optional challenges for extra learning (and bragging rights!)

Academic Integrity Policy

PROOF101 maintains a strict zero-tolerance policy for academic dishonesty, especially with respect to final mini-project submissions.

The following are considered violations:

• Copying work from another student (including line-by-line rewriting)
• Sharing solutions with other students
• Using code from the internet without proper attribution
• Unacknowledged use of LLMs (“vibe-coding” with AI assistance)

Permitted resources:

• Course materials, lectures, and textbooks
• Lean4 documentation and standard library
• Asking clarifying questions about problem statements
• Discussing high-level approaches (without sharing code)

Violations will result in:

• Zero credit for the assignment
• Ineligibility for Certificate of Distinction

When in doubt, ask! It’s always better to clarify.

Submission Guidelines

How to Submit

1. Complete your assignment in the provided .lean file
2. Test thoroughly (uncomment all test cases and verify they pass)
3. Email your solution to Daniel Dia at dmd13@mail.aub.edu
4. Subject line: PROOF101 Assignment [Number] - [Your Name]
5. Attach your completed .lean file

Deadlines

Assignments are typically due at the start of the next session unless otherwise specified.

Example: Assignment given Monday, January 26 → Due Monday, February 2

Late Submissions

If you cannot submit on time:

• Notify Daniel Dia in advance at dmd13@mail.aub.edu
• Explain your circumstances

Getting Help

Stuck on a problem? Here’s how to get unstuck:

1. Review course materials: lectures and readings often contain similar examples
2. Check the textbooks: they are very helpful and informative
3. Ask on Discord: post conceptual questions (not solution code)
4. Make good use of #check and #eval (Lean’s interactive feedback is your friend!)

Remember: Struggling is part of learning. Don’t be afraid to ask for help!

Good luck, and enjoy the challenge!