Automated Mathematical Theorem Proving

Mathematical discovery and reasoning is considered as the most creative activity of human wisdom. Mathematicians have been investigating the nature of human reasoning and problem solving. In particular, Polya published several books on this topic in 1960s, which are still very inspiring for current research. From 1970s, logicians and computer scientists have been investigating and developing so-called theorem provers to produce proofs automatically and to check human proofs using machines. Invented by de Bruijn, Automath is the first machine checkable language for expressing mathematics, and most modern interactive theorem provers are variants of Edinburgh LCF developed by Gordon and Milner. But there is still a gap between human and mechanical reasoning: precious human intelligence is spent on proving tedious and trivial theorems which are indispensable for machines to check the correctness and integrity of a proof.


We propose to shrink the gap by developing automated theorem provers for human reasoning. Except the automation of logic inference strategies and skills, the main planned innovations are: proving on abstract domains and generalising from cases. We will investigate and implement the mechanism to discover and exploit morphisms between algebraic systems, e.g., duality, quotient sets, Galois connection and insertion, etc., so as to simplify proofs by making use of collapsed structures. We want to equip the theorem prover with the generalisation capability such that they can explore known facts and develop conjectures from cases then prove or refute them automatically. We will adapt the equational proof style as the interface and the LCF style as the internal representation. By doing this, we are able to produce human readable and machine checkable proofs.


These innovations will potentially benefit the development of other research areas, including: search engines, design automation, neural computation, etc. Due to the mechanism of relying and learning from humans in case that the system is stuck, we are able to answer more complex queries, to avoid unnecessary searching, and to accelerate by exploit specific structures. We expect optimistically these benefits brought by techniques developed in this proposed research.