# Copyright makes no sense

Jump to navigation
Jump to search

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:

- At least one book is copyrighted (choose any book you can't download for free from the internet).
- At least one book is free (this article, for example).
- 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 constant copyrighted : set book -- 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₂) → b₂ ∈ copyrighted → b₁ ∈ copyrighted -- 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₁ }, contradiction, end