^^Proof assistant. LEAN. 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

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. Proof assistant.

Links

1. AlphaGeometry. AI at the IMO International Mathematical Olympiad.

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

Links inet

1. wp/Natural_deduction