SMT-based program verifiers provide powerful automation, but solver timeouts and unknown results can leave verification conditions unresolved. We introduce SMTLib-to-Lean, a tool that translates SMT-LIB queries into well-typed Lean~4 propositions, supporting both SMT and constrained Horn clause (CHC) problems. Using SMT-LIB as the interface lets existing verifiers reuse their SMT backends to send verification conditions to Lean~4 without implementing a verifier-specific Lean backend. Users can then construct kernel-checked proofs of satisfiability or unsatisfiability, manually or with AI assistance. We evaluate the tool on 2,935 benchmark inputs from SMT-COMP, CHC-COMP, and the TriCera benchmark suite.