^^Proof assistant. La matematica in linguaggio informatico.

La dimostrazione matematica in linguaggio informatico.

2025-05-21 Video che ha motivato la pagina

il video salta quasi alla fine dove spiega la situazione attuale, poiche' la parte introduttiva precedente e' troppo annacquata e non lineare, meglio altri video introduttivi.

• https://youtu.be/spIquD_mBFk?si=B_8TMkZvl8Wgxhcw&t=6282 The AI Math That Left Number Theorists Speechless

Wikify

1. wp/AlphaGeometry
   1. yt AlphaGeometry: An Olympiad-level AI system for geometry
2. AlphaProof Google_DeepMind#AlphaProof
   1. yt Thomas Hubert | AlphaProof: when reinforcement learning meets formal mathematics

voc: Dimostrazione matematica informatica.

≡ proof assistants

≡ interactive theorem provers

≡ systems for formalization

≡ Machine-Assisted Proofs

sono sistemi informatici che formalizzano la dimostrazione matematica in un linguaggio informatico.

LEAN  wp , https://lean-lang.org/about/

Lean is a proof assistant and a functional programming language.
It is based on the calculus of constructions with inductive types.
It is an open-source project hosted on GitHub.

1. https://functional.cafe/@leanprover Official account of the Lean theorem prover and programming language.
2. 2025-05-15 https://podcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai?video=1
   1. Math is now data that can be processed, transformed and inspected in various ways.
   2. Testing can only show the presence of the bugs, not the absence. - Edsger Wybe Dijkstra
   3. 2025-05-15 https://podcasts.ox.ac.uk/will-computers-prove-theorems?video=1
      1. What's math about? proving or underrstanding theorems? Do we just want to get the job done or do we want to understand whati's happening?
      2. This is this, is very, very wishy washy on exactly how this proof worked.
      3. Language models instead of cognition they are doing recognition. 
3. yt Terence Tao - Machine-Assisted Proofs (February 19, 2025)

Book: The Mechanics of Proof

https://hrmacbeth.github.io/math2001/

This is a book dealing with how to write careful, rigorous mathematical proofs.

From the preface

Interactive theorem-proving systems such as Lean have become steadily easier to use over the years, but they are not yet actually easy to use: they can be fussy and unforgiving, just like any other computer programming language. So why does this book propose that you use such a system in your first encounter with proofs?

The main novelty of this text is the “bilingual” presentation, juxtaposing prose mathematics with Lean code. But the design choices enforced by this presentation have shaped the text in other ways.

Links

1. Machine learning; apprendimento automatico.
2. Proof system.

Links inet

1. wp/Natural_deduction