Emulation Theory is a subject of math developed by Stanford Professor Harvey Friedman. In this project, we seek to formalise and prove several results in Emulation Theory using the theorem prover Lean
This work was done by Atticus Kuhn and Zongshu
To see how far along we are, look at ./src/basic.lean. I welcome all contributions and pull requests.