Developed a general one-dimensional quantum potentials module for the HEPLean/PhysLean repository, focusing on formal verification and mathematical physics using Lean. The work introduced momentum, position, and potential operators, along with a Schrödinger operator tailored for general 1D potential systems. Operator linearity was formally proven, ensuring mathematical rigor and correctness. A configurable parameter structure was implemented to manage system constants such as mass and Planck’s constant, supporting flexibility and reusability. The approach emphasized stability and traceability, linking changes to specific commits. No bugs were addressed during this period, with efforts concentrated on feature delivery and foundational quantum mechanics functionality.