Scientific machine learning methods such as neural operators and physics-informed neural networks are increasingly used to approximate solutions of complex PDEs, but their guarantees often stop at empirical accuracy. I will present TorchLean, a framework for neural networks and scientific computing in Lean 4, and discuss how we use it to formally reason about learned PDE solvers, automatic differentiation, and PDE residual computations. I will also describe our work on verified variable precision floating-point arithmetic in Lean, with the goal of connecting mathematical guarantees to the finite-precision computations that actually run in practice. Finally, I will discuss ongoing efforts to formalize parts of classical PDE analysis in Lean and to build symbolic tools for scientific reasoning. The broader goal is to connect PDE theory, learned models, and numerical computation within a common machine-checkable framework.