Theorem Provers

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

"Abstract: The formalisation of mathematics is an ongoing process that arguably started as early as the 19th century, intensified with the foundational crisis at the start of the 20th century, and since the 1970s has been conducted with the help of computers. Recent decades have seen the machine formalisation of lengthy and technically complicated proofs, but some have argued that even these were not representative of modern mathematics. Recent achievements by a number of different groups are starting to challenge this scepticism. The speaker will outline some of these, while also noting some of the remaining trouble spots.

This was the LMS-BCS FACS Seminar, which took place on Monday 15 January 2024 online via Zoom." - LMS YouTube Channel

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

Example in Isabella

For example, a declarative proof by contradiction in Isar that the square root of two is not rational can be written as follows.
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
By ,
Tags

No comments:

Post a Comment

Subscribe to: Post Comments (Atom)