2 + 2 = 4
- Problem ID:
two_plus_two - Test Problem: yes
- Submitter: Kim Morrison
- Notes: An easy problem to get you on the leaderboard.
- Source: Internal starter problem.
- Informal solution: By computation.
Do not modify Challenge.lean or Solution.lean. Those files are part of the
trusted benchmark and fixed by the repository.
Write your solution in Submission.lean and any additional local modules under
Submission/.
Participants may use Mathlib freely. Any helper code not already available in Mathlib must be inlined into the submission workspace.
Multi-file submissions are allowed through Submission.lean and additional local
modules under Submission/.
lake test runs comparator for this problem. The command expects a comparator
binary in PATH, or in the COMPARATOR_BIN environment variable.