*To*: <cl-isabelle-users at lists.cam.ac.uk>, <coq-club at inria.fr>, <acl2 at utlists.utexas.edu>, <pvs at csl.sri.com>, <theorem-provers at ai.mit.edu>, <agda at lis.ts.chalmers.se>, <stp at macs.hw.ac.uk>*Subject*: [isabelle] Industry researchers and engineer sought for new ATP/ITP project, Edinburgh UK*From*: David Aspinall <David.Aspinall at ed.ac.uk>*Date*: Fri, 18 Jun 2021 18:08:21 +0100*Arc-authentication-results*: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=ed.ac.uk; dmarc=pass action=none header.from=ed.ac.uk; dkim=pass header.d=ed.ac.uk; arc=none*Arc-message-signature*: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=aW1CxzbU2LFJjwYwPUnI4gw9Xhf1YFsh4qXEHr82qWU=; b=QTxq7CWHcTxp0cwcBz+9nO+zmV9wyXHDOAnRim/9TEhVqGbjVEm9N3M854dFKFs6Lav9JJUSZQEu7GB6JPA7uWyXzD/p101ueMeFUxB+iWCaIHoB9ligZt4NebDWrJ3QzZnS/r15/MrJBDrHggG1qE8EOjr9zgkolOqWhzwvxBGEMTnhrqIhYT5AVOL4QGQcT8PKTa5Ol/dp7Jv63w0YkDkBL85I+m+k3TX8OTF6mnRUmeQEdGAjmlf/aq0Gqyk1AS/XK7Dxislaq2L8NUJ3j9O/ncdkhnVFFwzpHkzIi8ekSjaQ58M003/33ekH70tFkYd66biXBrr8MSsHIy6/5w==*Arc-seal*: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=gqTBZTFBF7LHrrRXPC3I4KHGvOzghFUaa6cjIBdHqzRvHijFpfQEKLZKSOYvE4xeLFdbWHtHmpdk2KBUt2pQMxfG+rTA3BYWpKCuq8HXW8F/UM4aFwqpzi+9TNxFDRku6YcE1LHP1TizpxAYuReTQSv98Galk0UqdyTrKrd98581PgWsybBwJJsmZm4raOTTlDGqT1hIh4vkB0ko48UgPyd0xCpcuBFOSrwNJIjK6vZq56nJW8V8bY87VZQkaf5PXWwHhR2NpEFs3hSlzCQ7/MPW1bIWvodiDxRyGctYyU4vgTpbwOGrmnp2AsHhapj6zaQy2tYk+ZpOhCXNIQmxnw==*Authentication-results*: cam.ac.uk; iprev=pass (seine.is.ed.ac.uk) smtp.remote-ip=129.215.17.202; spf=pass smtp.mailfrom=ed.ac.uk; dkim=pass header.d=ed.ac.uk header.s=selector1 header.a=rsa-sha256; arc=pass (i=1) header.s=arcselector9901 arc.oldest-pass=1 smtp.remote-ip=129.215.17.202*Authentication-results*: huawei.com; dkim=none (message not signed) header.d=none; huawei.com; dmarc=none action=none header.from=ed.ac.uk;*Cc*: Wei Chen <weichen8 at huawei.com>*Reply-to*: Wei Chen <weichen8 at huawei.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

# A Gentle Invitation into Theorem Proving towards Formal Hardware Verification # What is the nature of human reasoning and problem solving? How can machines exploit the known skills of problems solving to solve new problems automatically? Is it possible to work out general patterns of discovery and reasoning, such that machines can develop new methods and systems? We try to answer these problems and shrink the gap between machine learning and human wisdom. Mathematical discovery and reasoning is considered the most creative activity of human wisdom. Mathematicians have been investigating the nature of human reasoning and problem solving since classical Greece. Even if the development of interactive theorem provers provides rigorous tools for people to formalise mathematics and to verify hardware and software designs, there is still a big gap between human reasoning and mechanical theorem proving: precious human intelligence is wasted on proving tedious and trivial lemmas, which are indispensable for machines to check the correctness and the integrity of a proof, but are quite obvious for well-educated mathematicians or computer scientists. Even worse, it is hard to recover the original intentions by reading these mechanical proofs. During the first year of this project, we will focus on developing an automated theorem prover towards human reasoning. Except the automation of proof strategies and skills, the main planned innovation is: deriving theories automatically. We want to investigate and implement such a mechanism: to generate conjectures from cases, concepts, proofs, and known theorems, then produce automatically human readable and machine checkable proofs. We also plan to design and implement the mechanism to discover and exploit morphisms between algebraic structures, so as to simplify proofs by making use of abstract domains. It doesn't mean that we don't need human interference; on the contrary, we want to make use of human experience whenever possible --- machines will learn from humans when, for example, they are stuck, the computation diverges, the solution space is too big, and so on. We believe that human skills of problem solving will enable machines to think like us and to make plausible reasoning at the end. We will soon open the following positions for this project. There will be a competitive salary and benefits package in line with top tier industrial R&D positions in UK. Work Location: Edinburgh UK 1. Two Full-Time Research Associates on Theoretical Computer Science. RA is supposed to hold a PhD degree. RA is required to have strong computer science background and has to be familiar with all branches of computer science in general. Research experience of formal verification, theorem provers, machine learning, programming languages, or compilers is necessary. RA will be responsible for the design and implementation of the proposed automated theorem prover, and its applications in automated formal verification of hardware and software designs. 2. A Full-Time Senior Software Engineer. SE is supposed to hold a BSc or MSc degree. SE is required to be familiar with the imperative programming languages like Python, the functional programming languages like Haskell, and the web programming languages like JavaScript. The development experience of programming languages is preferred. SE is responsible for the implementation, testing, and release of the proposed automated theorem prover. Also, we are recruiting interns on mathematics or computer science. We hope you can help create benchmarks or libraries, and improve the design and implementation of the tool. You are required to have a strong mathematical background. Basic programming skills of Haskell and Python are necessary. Knowledge of recursive functions, Lambda calculus, formal logics, type theory, or category theory is preferred. You are very welcome to join us on this ambitious exploration journey. Informal enquiries on details of the project and these positions can be made to: Dr. Wei Chen weichen8 at huawei.com Research Scientist on Theoretical Computer Science Hisilicon Advanced Research Department Huawei Edinburgh Research Centre The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

- Previous by Date: [isabelle] Proof Ground 2021 Call for Participation
- Next by Date: [isabelle] WiL'21 Final Call for Participation
- Previous by Thread: [isabelle] Proof Ground 2021 Call for Participation
- Next by Thread: [isabelle] WiL'21 Final Call for Participation
- Cl-isabelle-users June 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list