Questione di Scholze & Clausen

[megas_archon]

Questo è quello che intendevo quando dicevo "col tempo sarà impossibile distinguere il linguaggio naturale dal codice di una dimostrazione assistita": https://github.com/PatrickMassot/lean-v ... ample.lean

Questo testo è codice valido che compila:

Codice:

/-
If f is continuous at x₀ and the sequence u tends to x₀ then the sequence f ∘ u, sending n to
f (u n) tends to f x₀
-/
example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
 (hu : sequence_tendsto u x₀) (hf : continuous_function_at f x₀) :
 sequence_tendsto (f ∘ u) (f x₀) :=
begin
  Let's prove that ∀ ε > 0, ∃ N, ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
  Fix ε > 0,
  By hf applied to ε using ε_pos we obtain δ such that
    (δ_pos : δ > 0) (Hf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε),
  By hu applied to δ using δ_pos we obtain N such that Hu : ∀ n ≥ N, |u n - x₀| ≤ δ,
  Let's prove that N works : ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
  Fix n ≥ N,
  By Hf applied to u n it suffices to prove |u n - x₀| ≤ δ,
  This is Hu applied to n using n_ge,
end

Più che sottolineare che questa è la stessa matematica che scriviamo in TeX, ma è già proofreadata da una macchina, non saprei cosa dire.

[kaspar]

può essere utile leggersi l'HoTT book [...]?

Dipende da che "utilità". È una buona lettura, e alcune cose della parte "Mathematics" possono solo farti bene. Anche se non è matematica vera.
Puoi sempre provare, alla peggio lo molli se non ti interessa: succede niente.

[megas_archon]

Anche se non è matematica vera.

Waitwhat

[kaspar]

HoTT non è un modo per fare matematica "vera";

L'hai detto tu.
Mi rendo conto che un messagio scritto può essere recepito diversamente da quello pensato.
È ovvio, poi, che non so cosa sia la "matematica vera".

[megas_archon]

Quelle che intendevo è questo: un branch di agda, cubical-agda è una implementazione di HoTT, cioè di una certa interpretazione di MLTT. E' un adagio comune che "non si fa matematica in MLTT", perché è una fondazione un po' troppo rigida per fare le cose veramente. Questa, ad esempio, è una dimostrazione in standard-agda che 2+2=4:

Codice:

_ : plus · two · two —↠ `suc `suc `suc `suc `zero
_ =
  begin
    plus · two · two
  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
    (ƛ "m" ⇒ ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · two · two
  —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    (ƛ "n" ⇒
      case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
         · two
  —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]
  —→⟨ β-suc (V-suc V-zero) ⟩
    `suc (plus · `suc `zero · two)
  —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
    `suc ((ƛ "m" ⇒ ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · `suc `zero · two)
  —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
    `suc ((ƛ "n" ⇒
      case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · two)
  —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
    `suc (case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
  —→⟨ ξ-suc (β-suc V-zero) ⟩
    `suc `suc (plus · `zero · two)
  —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
    `suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · `zero · two)
  —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
    `suc `suc ((ƛ "n" ⇒
      case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · two)
  —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
    `suc `suc (case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
  —→⟨ ξ-suc (ξ-suc β-zero) ⟩
    `suc (`suc (`suc (`suc `zero)))
  ∎

(source: PLFA, https://plfa.github.io/Lambda/ )

Quella che ho postato oggi invece era una dimostrazione di analisi fatta in Lean, essenzialmente in linguaggio naturale. Puoi apprezzare la rigidità del primo linguaggio, e la flessibilità del secondo.

[kaspar]

Non è male dai...

Ecco sì, Agda non è sempre bello da leggere, visivamente. (Anzi, è molto brutto.) Su Lean si sta facendo molto lavoro per semplificare la vita all'utente --- o per nascondere molto lavoro sporco sotto il tappeto. D'altra parte non si può pretendere che un matematico conosca qualche TT. Oppure sì?

[megas_archon]

Non è male dai...

Ecco sì, Agda non è sempre bello da leggere, visivamente. (Anzi, è molto brutto.) Su Lean si sta facendo molto lavoro per semplificare la vita all'utente --- o per nascondere molto lavoro sporco sotto il tappeto. D'altra parte non si può pretendere che un matematico conosca qualche TT. Oppure sì?

perché no? Tutto serve... E soprattutto sapere un po' di teoria dei tipi rende attenti ai dettagli. Certe persone fanno matematica con la cazzuola.