The aim of an existence proof is simply to show something exists.
Task
Show there exists a natural number n, such that
$$n^{2}+1=10$$
You may see this written in mathematical notation, where the symbol \exists means “there exists”.
$$\exists n\in\mathbb{N}\;[n^{2}+1=10]$$
The essence of an existence proof is to demonstrate an object exists that satisfies any given conditions. Calculating, deriving, or even guessing, what that object is, is not the central point.
Maths
For our task, intuition tells us that $n$ can't be larger than $10$, and after some mental trial and error we find that $n=3$ works. We have found our example.
We don't need to justify how we arrived at our example. We only need to show it satisfies the condition $n^{2}+1=10$.
Let's write a proof, making clear each step.
$$\begin{align}\exists n\in\mathbb{N}\;&[n^{2}+1=10]&&\text{proof objective}\\&&&\\\text{use }n=3&&&\text{chosen example}\tag{1}\label{11.1}\\n^{2}+1&=(3)^{2}+1&&\text{using }(\ref{11.1})\\&=10&&\text{by arithmetic }\tag*{\(\Box\)}\end{align}$$
We first state the proof objective, which includes the condition $n^{2}+1=10$ any example must meet.
We then choose $n=3$, and show by arithmetic that indeed $n^{2}+1=10$.
Code
The following Lean program proves there exists a natural number $n$ such that $n^{2}+1=10$.
-- 11 - Existence proof
import Mathlib.Tactic
example : ∃ n: ℕ, n^2 + 1 = 10 := by
use 3
calc
3^2 + 1 = 10 := by norm_num
The proof header is a little different from the ones we've looked at recently. Here, there is no separate definition of variable types, and no hypothesis. The entire theorem is in the proof objective.
The proof objective ∃ n: ℕ, n^2 + 1 = 10 says that there exists a natural number n, such that n^2 + 1 = 10.
The next step is to choose an example that meets this condition. The instruction use 3 tells Lean that we propose 3 as that example.
The Infoview will confirm that use 3 changes the proof goal from ∃ n, n^2 + 1 = 10 to 3^2 + 1 = 10.
We can use a simple calc section to show by arithmetic that 3^2 + 1 is indeed 10, completing the proof.
Bad Example
Let's see what happens if we choose a bad example, say $n=4$. This means changing the code to use 4.
Placing the cursor after use 4 shows the proof goal.
⊢ 4 ^ 2 + 1 = 10
This goal is impossible to prove, because $17$ is not $10$.
Simpler Code
The following is a shorter version of our Lean program.
-- 11 - Existence proof
import Mathlib.Tactic
example : ∃ n: ℕ, n^2 + 1 = 10 := by
use 3
norm_num
The goal at the point of the previous calc section was ⊢ 3^2 + 1 = 10. This is simple enough to apply the norm_num tactic to prove. It doesn't really need a calc section, which is better suited to derivations that require several steps.
As with all code, it is better to be clear and unambiguous than overly concise. This use of one-line tactics should only be done when the context is simple and clear for anyone reading your code - including your future self.
Easy Exercise
Write a Lean program to prove there exists a natural number greater than $5$.
In mathematical notation, the proof objective is as follows, and should translate into Lean code fairly directly.
$$\exists n\in\mathbb{N}\;[n>5]$$
As an optional extra challenge, try writing the proof in the concise form shown above.
