About by Alcides Fonseca
Logic ForAll
Index
The formal verification of computer systems has become practical. It has an essential role in tech firms such as Amazon, AMD, Intel, Microsoft and Nvidia. In recent years, researchers have started asking whether verification technology could also benefit research mathematicians. Here, we explore every aspect of doing logic on the computer: its foundations, its applications and the issues involved with formalising mathematics.
One of the my first posts described ALEXANDRIA , my ERC Advanced Grant aiming to bring verification technology to professional mathematicians. This project ends on 31 August 2023 (extended by a year on account of the pandemic), so it’s surely time to update the community on what has been accomplished. As outlined in the earlier post, our starting point was a growing acceptance of the prevalence of errors in mathematics, along with a small body of formal mathematical developments that had been undertaken in
In a blog devoted to mathematics and logic, it’s hard to avoid Wittgenstein. Wittgenstein saw his main contributions being to the philosophy of mathematics and logic. I’m not sure that he understood either of them. But let’s begin with natural science, since it touches on topics relevant to this blog, such as the relationship between models and the real world . Natural science is another field where Wittgenstein indulged in his habit of obscurantism. Since I don’t know much about philosophy, perhaps I have
About by Alcides Fonseca
Logic ForAll
Index