Researcher ORCID Identifier
Graduation Year
2023
Document Type
Campus Only Senior Thesis
Degree Name
Bachelor of Science
Department
Mathematics
Reader 1
Weiqing Gu
Reader 2
Heather Zinn Brooks
Terms of Use & License Information
Abstract
We have formalized definitions and results from discrete exterior calculus — a generalization of calculus to curved meshes — in the interactive theorem prover Lean. This thesis serves as a simultaneous introduction to both computer-assisted proof verification and the field of discrete differential geometry.
Recommended Citation
Thum, Maxwell, "Formalizing Discrete Exterior Calculus in Lean" (2023). HMC Senior Theses. 282.
https://scholarship.claremont.edu/hmc_theses/282
Data Repository Link
https://github.com/maxwell-thum/DDG_Lean3/tree/20bf885c2ed62267939aae6600a7f6ed4a53090b
Poster
This thesis is restricted to the Claremont Colleges current faculty, students, and staff.
