NanoProof is a dependently typed proof checker implemented as a single Haskell file that supports dependent function types (Pi), dependent pairs (Sigma), equality types, and recursive definitions through fixpoints and guarded recursion. The system includes a collection of base types such as the empty type, unit type, and bit type, along with support for equality proofs via reflexivity and rewriting. NanoProof deliberately omits a termination checker, placing responsibility on users to ensure their recursive definitions are terminating or productive.