Classical Isoperimetric Theorem

In this article we present the Mizar proof of the isoperimetric theorem (one of the theorems listed among Wiedijk’s Top 100 mathematical theorems), inspired by Peter D. Lax’s paper “A Short Path to the Shortest Path”. Using relatively simple formal apparatus of continuous and differentiable functions, we show that among all curves of fixed length connecting two points on the x-axis, a semicircle is the curve which maximizes the area between the curve and the x-axis.