# Interactive Proof Presentations with Cobra

## TL;DR

Cobra is an innovative proof presentation framework that combines advanced presentation tools with an interactive theorem prover, enabling live, interactive, and verifiable formalized mathematics presentations.

## Contribution

It introduces Cobra, a novel system that integrates live theorem proving with interactive presentation technology for formalized mathematics.

## Key findings

- Live proof checking during presentations enhances accuracy.
- Audience interaction allows real-time modifications to proofs.
- Cobra facilitates engaging and verifiable mathematical talks.

## Abstract

We present Cobra, a modern proof presentation framework, leveraging cutting-edge presentation technology together with a state of the art interactive theorem prover to present formalized mathematics as active documents. Cobra provides both an easy way to present proofs and a novel approach to auditorium interaction. The presentation is checked live by the theorem prover, and moreover allows for live changes both by the presenter and the audience.