I think this approach to bug hunting is super promising (obviously - it finds a ton of bugs). The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. The approach taken by these people, the same approach as when the Julia folks did it, isn't really automatable, because it requires a lot of both human and AI agent work.
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
stabbles 13 minutes ago [-]
At that point you might as well use Lean?
It would solve the two language problem :-)
eternauta3k 2 hours ago [-]
Is there a way to avoid the translation or replace it with normal parsing?
choeger 2 hours ago [-]
In principle, yes.
I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.
perching_aix 1 hours ago [-]
it's a matter of how much of a modeling gap do you choose to accept.
for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.
just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.
bb88 2 hours ago [-]
Only 418?
I would have expected around 10k.
Edit: Professional python programmer.
perching_aix 1 hours ago [-]
they don't have full coverage yet
senderista 2 hours ago [-]
Cite an AI-written document? Hell no.
up2isomorphism 2 hours ago [-]
AI does not kill research, research kills pretty much itself already.
woggy 2 hours ago [-]
Can we just develop in Lean and compile to something else for speed?
iib 1 hours ago [-]
Lean is actually pretty speedy as is, and it enables much harder optimizations[1]
Some parts of this are true, but bringing up z3 is kind of a random tangent without any actual knowledge to be shared behind it.
perching_aix 2 hours ago [-]
formal modeling and verification doesn't become 100% magically useless just because you can't assert semantic correspondence automatically. one would expect a champion of understanding to understand this.
way to take issue with credibility from a blatant sockpuppet account by the way. like, really dude?
fny 3 hours ago [-]
[flagged]
echelon 2 hours ago [-]
Stop using the word slop. It's a joke at this point.
creata 1 hours ago [-]
No offense, but that doesn't mean a whole lot coming from someone who's all in on the slop train, ArtCraft guy.
tomhow 1 hours ago [-]
> ArtCraft guy.
Please don’t post comments with snarky stings in the tail on HN. Disagreement is fine. Personal swipes are definitely not.
It's not a snarky sting. I think ArtCraft is very impressive, to be clear. I just couldn't figure out another concise way to provide the relevant context that would be needed to understand my comment.
Now if I did want to be snarky, this is the part where I'd point to the "assume good faith" part of the guidelines.
nurettin 3 hours ago [-]
Title says formalizing, article amounts to "we asked claude to check one result with lean, got bad results, then we told it to make no mistakes".
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
It would solve the two language problem :-)
I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.
for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.
just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.
I would have expected around 10k.
Edit: Professional python programmer.
[1] https://github.com/kim-em/lean-zip#verification-enables-perf...
way to take issue with credibility from a blatant sockpuppet account by the way. like, really dude?
Please don’t post comments with snarky stings in the tail on HN. Disagreement is fine. Personal swipes are definitely not.
https://news.ycombinator.com/newsguidelines.html
Now if I did want to be snarky, this is the part where I'd point to the "assume good faith" part of the guidelines.