Right and these are perfect math objects: a perfect sphere has only one parameter. You can't describe a real life ball in Lean. You may be able to describe a class of real life balls using probability theory.