Linear Algebra in Isabelle/HOL

Linear Algebra in Isabelle/HOL

The main purpose of this event will be to survey the different formalisations and developments of Linear Algebra in Isabelle/HOL and to explore the possibilities of communicating them and improve the representations currently used.  In the following links can be found the programme and the announcing poster.

Dates: 15 – 17 November

Organisers (please contact us for any further information):

Jesús María Aransay Azofra (

Jose Divasón Mallagaray (

List of Participants:

Lawrence Paulson (Cambrige University)

Angeliki Koutsoukou-Argyraki (Cambridge University)

René Thiemann (University of Innsbruck)

Johannes Hölzl (Vrije Universiteit Amsterdam)

Mohammad Abdulaziz (Technische Universität München)

Fabial Immler (Technische Universität München)

Manuel Eberl (Technische Universität München)

The followig talks will be part of the programme (see the links for details):

René Thiemann. The Perron-Frobenius Theorem in Isabelle/HOL. Transferring between matrix representations.

Fabian Immler. Rigorous Numerics and Linear Algebra In Isabelle/HOL.

Johannes Hölzl. Recent developments in Lean and its analysis.

Manuel Eberl. Semi-automatic asymptotics in Isabelle/HOL.

Mohammad Abdulaziz. An Isabelle/HOL formalisation of Green’s Theorem.

This event has been partially funded by the programme Erasmus+, the project MTM2014-54151-P from “Ministerio de Economía y Competitividad (Gobierno de España)”, and the “Vicerrectorado de Investigación” of “Universidad de La Rioja”. The “Departamento de Matemáticas y Computación” of “Universidad de La Rioja” also has contributed to the event by facilitating the required equipment.

Universidad de La Rioja


Ministerio de Economía y Competitividad