La dimostrazione matematica in linguaggio informatico.
https://youtu.be/spIquD_mBFk?si=B_8TMkZvl8Wgxhcw&t=6282 The AI Math That Left Number Theorists Speechless
proof assistants
interactive theorem provers
systems for formalization
sono sistemi informatici che formalizzano la dimostrazione matematica in un linguaggio informatico.
https://hrmacbeth.github.io/math2001/
This is a book dealing with how to write careful, rigorous mathematical proofs.
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.