Deep Learning and Mathematical proof checking

AI, in particular Deep Learning, has been transformed the world very fast. AI models now works very well in various fields: image, sound and video analysis, and are incorporated in many products worldwide. More recently, the phenomenon of ChatGPT and Large Language Models (LLM) has been a hot topic. 

One crucial step to making intelligent AI agents, who can share many duties with us (like driving cars or controlling spaceships), is to make them excel in logical arguments. Given we have LLM, it is natural to think that the Ais can already do good logical arguments. Not quite so, many experiments show the opposite! There is an inherent incompatibility between how AI works (relies on probability/statistics) and logics works (requires absolute precision). This project is to combines AI and logics in an appropriate form to help with verifying mathematical proofs, one first step towards having truly intelligent AIs.

Even mathematical journals now acknowledge that they have difficulty with finding enough careful and diligent referees/reviewers to check that proofs of results in submitted papers are correct. Not to mention many preprints out there. Humans are prone to checking long and tedious details, which are present and necessary in mathematical proofs, in particular those new and have a lot of applications.