lanyonai/advectiondiffusion

This repository holds a set of solvers for advection and diffusion equations, which are mathematical equations used to describe how a quantity, like heat or a dissolved substance, spreads and moves through space over time. The project covers three versions of the problem: simple linear advection, advection combined with diffusion that behaves the same in every direction, and a fuller version where diffusion can behave differently depending on direction. Each version is solved in one, two, and three dimensions, giving nine solvers in total. What makes this project unusual is that every solver comes with a formal, machine checked proof of correctness. The proofs are written in Lean 4, a programming language built for verifying mathematical statements, and the repository reports close to 9,600 lines of that proof code alongside roughly 8,300 lines of the actual C code that runs the simulations. The README states there are 438 definitions and 282 theorems backing the correctness claims. All of this, both the C solvers and their Lean proofs, was generated by a tool called Lanyon in about 156 seconds total, with individual solvers taking anywhere from about 7 to 31 seconds each. The README includes the general mathematical form of the advection-diffusion equation and links to a separate technical writeup on the Lanyon website that covers the numerical methods and the prompts used to produce the code. It also includes screen captures and images showing example solutions, such as a one dimensional case on a periodic domain and a two dimensional case showing a shape being carried along by a rotating flow. This project will mainly interest people working in scientific computing, numerical methods, or formal verification who want to see machine generated, proven correct simulation code. It assumes familiarity with partial differential equations and is not aimed at general audiences. No license file or explicit usage instructions are mentioned in the README shown here.