| Homepage | https://www.joachim-breitner.de/blog |
| GitHub | https://github.com/nomeata |
RE: https://discuss.systems/@bobkonf/116221261428106677
I showed up this morning at breakfast at #bobkonf looking forward to some relaxed listening to tasks, when the organizer approached me and asked if can spontaneously fill a slot. So I did and gave a #leanProver talk. This keeps happening to me, that's how I ended up giving a talk here last year 🤷🏻
RE: https://mastodon.social/@fm_volker/116205304864670485
AI can be brutally honest: about how little human intelligence some of our daily tasks actually need, about how incomplete human peer review is, and how fig-leafy some anonymization attempts are. Maybe that’s a good thing.
I participated into a study on how I use Lean They anonymized the transcript for some research repository, and asked me to approve that. I pasted that transscript into Gemini, and immediately got:
SPEAKER_01 is an advanced user and developer of the Lean theorem prover.
While the transcript doesn't explicitly state a name, the speaker provides very specific biographical and technical details that strongly suggest they are Joachim Breitner.
Key Identifying Details: […]
Anonymization is hard.
In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two Higgs doublet model (2HDM) potential. Twenty years on, it is now easier to apply the process of formalization into an interactive theorem prover to this work thanks to projects like Mathlib and PhysLib (formerly PhysLean and Lean-QuantumInfo), and to ask for a higher standard of mathematical correctness. Doing so has revealed an error in the arguments of this 2006 paper, invalidating their main theorem on the stability of the 2HDM potential. This case is noteworthy because to the best of our knowledge it is the first non-trivial error in a physics paper found through formalization. It was one of the first papers where formalization was attempted, which raises the uncomfortable question of how many physics papers would not pass this higher level of scrutiny.
@jeanas writes "I want it to translate the recursion to eliminators (it doesn't necessarily mean that the recursion disappears from the core language but there should be a check that this can be done in some way)."
+1.
I wish this was available for Agda.
But also the above is why I have been always suspicious of corecursion in proof assistants. We understand this categorically, but the way it is done in any proof assistant feels like a hack to me.
@mevenlennonbertrand here is a full account of what was found (collaboration between Opus 4.6 and rocq experts):
- 3 proofs of false from bugs in the guard checker
- 2 proofs of false from bugs in the module system (the second one uses Girard's paradox)
- 1 proof of false from a bug in `conversion.ml`
- 1 proof of false from a bug in `discharge.ml` (using Hurkens' paradox)
- 1 anomaly from a bug in `conversion.ml`
- 2 bugs in `cClosure.ml`
- 1 bug in `mod_declarations.ml`
jcreed
Martin Escardo
cosmo
