Explore data-parallel proof verification in a 20-minute conference talk from Dyalog '24 that demonstrates how APL can be leveraged for efficient mathematical proof verification using Metamath. Learn about formal verification systems, their history, and how mathematical proofs can be rigorously verified using computer-processable language. Discover the process of proving basic mathematical concepts like 2+2=4 through simple replacement, understand proof tree structures, and see practical examples in Metamath. Follow along as the conversion of Metamath proofs into tree structures is explained, and examine the performance aspects of verifying large proof databases. The presentation includes detailed slides available in both Prezi and PDF formats, making it easier to grasp the concepts of data-parallel processing in mathematical proof verification, a unique approach not found in existing Metamath systems.
Data Parallel Proof Verification in APL - Using Metamath for Mathematical Databases
Dyalog User Meetings via YouTube
Overview
Syllabus
Formal verification and informal proofs
The landscape of formal verification
History of formal verification systems
Prove 2+2=4 with simple replacement
Proof as a tree structure
Example in Metamath
How to convert a Metamath proof into a tree
Speed of verifying proof databases
Recap and future work
Taught by
Dyalog User Meetings
