### Mikes Notes

I have a fortnightly online meeting with my computer scientist friends Alex and Chris to discuss our various computer and mathematics projects. It is an excellent way of getting feedback and being exposed to new ideas.

Earlier this year, Alex mentioned an online talk at the London Mathematical Society that he attended. I then watched it. It was about "proving assistants," AKA "theorem provers."

I find mathematics papers unfathomable. But I could follow along quite easily reading the proofs generated by Isabella, the proving assistant.

"Automated theorem proving (also known as ATP or automated deduction) is a
subfield of automated reasoning and mathematical logic dealing with proving
mathematical theorems by computer programs. Automated reasoning over
mathematical proof was a major impetus for the development of computer
science." - **Wikipedia**.

#### Isabella

#### Vampire

"**Abstract:** Vampire is a fully automated theorem prover for
first-order logic that has been developed for over 25 years. It has a long
tradition of being the “best” in the world (solves the most in the least
time at the theorem prover competition) for traditional first-order logic
problems found in many domains. However, this traditional first-order logic
setting often struggles to capture problems from program verification that
need to talk about theories such as arithmetic. Indeed, program verification
is typically the domain of SMT solvers (Boolean SAT solvers extended with
theory decision procedures). However, we often see problems in program
verification that combine theories and quantification (the bread-and-butter
of traditional first-order logic reasoning) where SMT solvers struggle with
heuristic approaches. Therefore, around 10 years ago we embarked on a
journey to extend Vampire to the program verification space, adding theory
reasoning, induction, interpolation, and a some other fun things. It is this
journey, the challenges, advances, and applications, that I will talk about
in this presentation

Part of the LMS Computer Science Colloquium 2023, which took place on Friday 1 December 2023 at De Morgan House, London and online via Zoom." - LMS YouTube Channel

### Resources

- London Mathematical Society
- https://www.youtube.com/@LondonMathematicalSociety
- The Vampire Journey: building a theorem prover for program verification, Giles Reger | LMS CSC 2023 (7 Feb 2024)
- Theorem Prover
- Vampire
- Formalising 21st-Century Mathematics, Lawrence C. Paulson FRS | LMS/BCS-FACS Seminar 2024 (15 Jan 2024)
- Lawrence Paulson
- Isabella

### Example in Isabella

```
theorem sqrt2_not_rational:
"sqrt 2 ∉ ℚ"
proof
let ?x = "sqrt 2"
assume "?x ∈ ℚ"
then obtain m n :: nat where
sqrt_rat: "¦?x¦ = m / n" and lowest_terms: "coprime m n"
by (rule Rats_abs_nat_div_natE)
hence "m^2 = ?x^2 * n^2" by (auto simp add: power2_eq_square)
hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce
hence "2 dvd m^2" by simp
hence "2 dvd m" by simp
have "2 dvd n" proof -
from ‹2 dvd m› obtain k where "m = 2 * k" ..
with eq have "2 * n^2 = 2^2 * k^2" by simp
hence "2 dvd n^2" by simp
thus "2 dvd n" by simp
qed
with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest)
with lowest_terms have "2 dvd 1" by simp
thus False using odd_one by blast
qed
```

## No comments:

## Post a Comment