PhysicalMathematics

A formal mathematics project exploring physical mathematics concepts using the Lean theorem prover.

References

https://en.wikipedia.org/wiki/Quantum_group

https://terrytao.wordpress.com/wp-content/uploads/2018/08/webinar.pdf

Concepts

An incomplete system is self-consistent and not self-referential. I thought Mathemics is pure and not stateful. A condense matter. It is simpler to test a pure function in a unit. Turning machine is stateful. λ-calculus lacks of mutable state. 熱門(logic gate)

"Vaporizing and freezing the Riemann zeta function" - 陶哲軒

實驗;熱力學;數態

Lean Project

This repository includes formalized mathematical proofs using Lean 4. The project explores concepts related to:

• Pure functions and their properties
• λ-calculus fundamentals
• Mathematical consistency

Prerequisites

• Lean 4 (version 4.12.0)
• Lake (Lean's build system, included with Lean 4)

Building the Project

lake build

Running the Project

lake exe physical-mathematics

Project Structure

• PhysicalMathematics/Basic.lean - Foundational definitions and theorems about pure functions and λ-calculus
• Main.lean - Entry point for the executable
• lakefile.lean - Lake build configuration