In this article we prove that copyright does not make any sense. Not only that we prove it, but we also verify the proof using Lean theorem prover. The proof is 100% correct!

### Definitions

A book is a finite list of symbols (a symbol is a natural number, for simplicity). There exists a set of all copyrighted books. Also, there exists a set of all free books (in this context, by "free" we mean "public domain").

### Axioms

All lawyers that I asked told me there are three axioms:

3. If you have some book and there is a reliable way that you can reconstruct a copyrighted book from it, then that book is copyrighted too.

### Theorem

If those axioms are consistent, zero is equal to one.

### Proof

```-- Lean: v3.42.0
-- Mathlib: b6d246a6

import tactic

-- A book is a sequence of symbols
def book : Type := list ℕ

-- There is a set of all copyrighted books

-- And the set of all free books (public domain)
def free : set book := set.univ \ copyrighted

-- At least one book is copyrighted
axiom exi_cop : ∃ (b : book), b ∈ copyrighted

-- At least one book is free
axiom exi_free : ∃ (b : book), b ∈ free

-- If you can reconstruct a copyrighted book from some other book,
-- then that book is copyrighted too
axiom copy_tran : ∀ (b₁ b₂ : book), (∃ (f : book → book), f b₁ = b₂) →

-- Copyright makes no sense! (CONFIRMED)
lemma copyright_makes_no_sense : 0 = 1 :=
begin
obtain ⟨b₁, h₁⟩ := exi_cop,
obtain ⟨b₂, h₂⟩ := exi_free,
have h₃ : b₂ ∉ copyrighted,
{ simp [free] at h₂, exact h₂ },
have h₄ : b₂ ∈ copyrighted,
{ exact copy_tran b₂ b₁ ⟨λ _, b₁, rfl⟩ h₁ },