[FOM] proof assistants and foundations of mathematics

[Lawrence Paulson]

You might like to read my paper on such topics:

https://arxiv.org/abs/1804.07860

Larry

> On 6 Aug 2018, at 20:04, José Manuel Rodriguez Caballero <josephcmac at gmail.com> wrote:
> 
> My formation is mainly in pure mathematics (number theory), not in foundations of mathematics. So, I'm rather curious of some results that could be not interested at all for people with a solid formation in foundations of mathematics: I'm just learning from the answers in FOM and MetaMath groups and I'm understanding better the proof assistants from the point of view of foundations of mathematics. I'm not claiming any inconsistency in Coq, I'm just comparing this possibility with the possibility of inconsistency of Q0. For me the inconsistency of Coq is a rather theological claim.