Doctoral Thesis
Abstract
This thesis explores the intersection of formal mathematics, artificial intelligence, and scientific research. By leveraging the Lean theorem prover, we demonstrate how formalized mathematical theories can enhance AI systems and advance scientific discovery across multiple domains.
Research Questions
- How can formal verification improve the reliability of AI systems in scientific applications?
- What are effective methodologies for translating scientific theories into formal mathematical frameworks?
- How can interactive theorem proving facilitate interdisciplinary collaboration between mathematics, computer science, and natural sciences?
Methodology
Our approach combines formal methods from computer science with techniques from machine learning and domain-specific scientific knowledge. We develop new libraries in the Lean theorem prover to represent scientific theories and validate AI-generated hypotheses.
Chapters
Chapter 1: Introduction to Formal Mathematics in Scientific Computing
Draft Complete
Chapter 2: Lean Theorem Prover: Architecture and Applications
In Progress
Chapter 3: Formalizing Physical Theories
Planned
Chapter 4: Machine Learning with Formal Guarantees
Planned
Chapter 5: Case Studies in Scientific Discovery
Planned
Chapter 6: Conclusions and Future Work
Planned
Publications
Related publications will appear here as they become available.