[Club2] Mon Oct. 18, 16:00: [Grechuk Bogdan] Isabelle as a Proof Assistant for Mathematicians

[Johannes Hölzl]

Hi Club 2,

Grechuk Bogdan will visit us on Oct. 18 and give a talk in room
00.11.038 (John v. Neumann) at 16:00.

=========================================

Title:  Isabelle as a Proof Assistant for Mathematicians

Abstract: I will discuss my formalization of some results of convex
analysis in Isabelle, and give  suggestions on how to make Isabelle more
attractive for mathematical community. Together with very global and
general  questions,  like organization of search in Isabelle, I will
give some very specific suggestions, which would be very helpful in this
and similar mathematical formalizations. In particular, I suggest tactic
to do “Proof by analogy”, which would make the formalization much
easier, and would help to avoid bad-looking repetitions in the proof
script.   

=========================================-

- Johannes