lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"

12 stars 0 forks source link

https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijection_example.html #44

Open utterances-bot opened 4 months ago

utterances-bot commented 4 months ago

Two Small Examples by Fields Medallists

https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijection_example.html

SKolodynski commented 4 months ago

I have added an Isabelle/ZF proof of the Gowers' example as lemma bij_def_alt to IsarMathLib as an example of a more detailed, structured Isar - style proof for comparison.