A formalisation of Solèr's theorem using the Isabelle proof assistant
Work-in progress - this is currently a playground for me learning Isabelle
git clone https://github.com/michalc/solers-theorem
cd solers-theoremYou must also have Docker installed.
On an x86 (e.g. intel)
docker run -v $PWD/Solers.thy:/home/isabelle/Solers.thy makarius/isabelle:Isabelle2022 process -T SolersOn ARM (e.g. Apple M1)
docker run -v $PWD/Solers.thy:/home/isabelle/Solers.thy makarius/isabelle:Isabelle2022_ARM process -T Solers