Philippe Thomas Savard (Jan 27 2026 at 04:44): Philippe Thomas Savard (Jan 27 2026 at 04:44):Hello everyone,
I am a newcomer to Isabelle/HOL and I am currently stuck while trying to formalize a personal project called "The Geometry of the Prime Number Spectrum." My goal is to explore a specific distribution (1/2) between prime numbers.
I am not a trained mathematician or an Isabelle expert, so I would appreciate it if someone could help me with a very patient and simple approach, as I might struggle with advanced technical explanations.
The situation: Yesterday, I almost managed to generate a LaTeX PDF from Isabelle, which took about 4 hours and 26 minutes to compile. However, after trying to fix two minor errors (which looked like Unicode errors), everything broke. Now, I cannot even run a 15-second compilation without everything failing. My attempts to fix it myself have only made the situation worse.
I have uploaded my code here:
geometrie_spectre_premier (2).zip
If someone could spare some time to look at my code and tell me what is wrong, I would be very grateful. Please don't expect too much from me regarding Isabelle basics, as I am still very much learning the fundamentals.
Thank you in advance for your kindness and help!
Best regards, Philippe"
Maximilian Schäffeler (Jan 27 2026 at 11:27):Hi Philippe,
before attempting to generate a LaTeX PDF, I would first try to fix the proofs: several of your by simp proof attempts either don't terminate or do not prove the goal (I am using Isabelle 2025-2). Also, in the definition of spectral_list you should replace \leftrightarrow with \longleftrightarrow.
Maxi
Last updated: Feb 12 2026 at 20:37 UTC