Basic Hilbert

A Lean 4 experiment.