#formalmath — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #formalmath, aggregated by home.social.
-
A computer found one solution to a hard model-building problem. Then we proved you will *always* find one — and machine-checked the proof in Lean 4. 🧮
The setting: which fermions complete a quark block in a 6D \(SU(4)\) gauge–Higgs model on an orbifold, so that every local consistency condition (anomalies + "tadpoles") cancels? These are exact integer / representation-theory conditions over \(SU(4)\) weights.
One witness is easy to distrust — a fluke? The structural answer is no. Writing the anomaly map \(A\) and the tadpole map \(\Theta\) as linear functionals of the added matter, two exact facts settle it:
• \(\operatorname{rank}[A;\Theta]=8+2=10\): the tadpole is *independent* of the anomalies — no conserved invariant traps it;
• anomaly-neutral additions realise *every* tadpole direction (Farkas certificates), so their cone is all of \(\mathbb{R}^2\).Hence *every* anomaly-free completion is tadpole-compatible: an Existence theorem, not luck. The certificate is checked by the Lean 4 kernel, depending only on propext. The same rank+cone test ships as a reusable tool for any orbifold model. Honest scope: one infrared step stays open.
📄 https://zenodo.org/records/21432626
💻 https://github.com/karlesmarin/ghu-su4-completion#Lean4 #FormalMath #ProofAssistant #RepresentationTheory #Maths #Physics
-
A computer found one solution to a hard model-building problem. Then we proved you will *always* find one — and machine-checked the proof in Lean 4. 🧮
The setting: which fermions complete a quark block in a 6D \(SU(4)\) gauge–Higgs model on an orbifold, so that every local consistency condition (anomalies + "tadpoles") cancels? These are exact integer / representation-theory conditions over \(SU(4)\) weights.
One witness is easy to distrust — a fluke? The structural answer is no. Writing the anomaly map \(A\) and the tadpole map \(\Theta\) as linear functionals of the added matter, two exact facts settle it:
• \(\operatorname{rank}[A;\Theta]=8+2=10\): the tadpole is *independent* of the anomalies — no conserved invariant traps it;
• anomaly-neutral additions realise *every* tadpole direction (Farkas certificates), so their cone is all of \(\mathbb{R}^2\).Hence *every* anomaly-free completion is tadpole-compatible: an Existence theorem, not luck. The certificate is checked by the Lean 4 kernel, depending only on propext. The same rank+cone test ships as a reusable tool for any orbifold model. Honest scope: one infrared step stays open.
📄 https://zenodo.org/records/21432626
💻 https://github.com/karlesmarin/ghu-su4-completion#Lean4 #FormalMath #ProofAssistant #RepresentationTheory #Maths #Physics
-
We’re pleased to announce #ItaLean2025: Bridging Formal Mathematics and AI, an international conference dedicated to @leanprover, Formal Mathematics, and AI4Math.
📍 University of Bologna
🗓 9–12 December 2025#ItaLean2025 brings together researchers and practitioners advancing the formalization of mathematics in Lean and exploring the interplay between machine learning and formal methods.
The program includes lectures, tutorials, research talks, product demos, and a concluding panel.
Applications to participate are now open.
Participation is free of charge.A limited amount of travel support may be available.
Priority deadline: 31 October 2025.A preliminary schedule will be released in the coming weeks, with regular updates to follow.
Official website (applications, program, logistics): https://pitmonticone.github.io/ItaLean2025/