3 ms·

Thanks for writing such an elaborate reply! I wish I was familiar with Lean, so I could follow. But if you're right, it would put the claims of the paper in a t

by kleiba 7mo ago

Thanks for writing such an elaborate reply! I wish I was familiar with Lean, so I could follow. But if you're right, it would put the claims of the paper in a totally different light. Perhaps others with knowledge in Lean could also chime in?

refulgentis 7mo ago
Doubtful: - articles two days old - I got links right to the code - its clearly a waste of time if you know Lean, I went way above and beyond already Maybe if you were able to show "no actually > 0 of this is well founded", someone might be tempted. But you'd need someone who showed up days later, knows enough Lean to validate for you, yet, not enough Lean to know it's a joke just from looking at the links. You're welcome! Don't mean to be mean (pun intended), hope you don't read it that way. Just, figured it'd give you some food for thought re: exactly how much work you can expect from other people, and that you might need to set more constraints on an "idk, can someone else tell me more?" reaction than "one person said something, but someone else said they're wrong, so score is 1 to 1"
- kleiba 7mo ago
  Thanks again - this time I have to admit I really don't get what you're trying to say?!
  - refulgentis 7mo ago
    Sorry, I was unclear! You said you wished someone with Lean knowledge could check my work. I'm saying: you can check it yourself, right now, without knowing Lean. Click any of links [2] through [5]. You'll see the word `axiom` in the code. In Lean, `axiom` means "assume this is true without proof." That's it. That's the whole critique. The paper says "formally verified," but the key claims — FFN computes Bayesian update, attention routes correctly, BP converges, no hallucination — are all just assumed. You don't need to take my word for it, and you don't need a Lean expert to break a tie. The evidence is right there in the links. It'd be like a paper claiming "we formally proved this bridge is safe" and the proof says "Axiom: this bridge is safe." You don't need a civil engineer to tell you that's not a proof.

by kleiba 7mo ago

refulgentis 7mo ago

Doubtful: - articles two days old - I got links right to the code - its clearly a waste of time if you know Lean, I went way above and beyond already Maybe if you were able to show "no actually > 0 of this is well founded", someone might be tempted. But you'd need someone who showed up days later, knows enough Lean to validate for you, yet, not enough Lean to know it's a joke just from looking at the links. You're welcome! Don't mean to be mean (pun intended), hope you don't read it that way. Just, figured it'd give you some food for thought re: exactly how much work you can expect from other people, and that you might need to set more constraints on an "idk, can someone else tell me more?" reaction than "one person said something, but someone else said they're wrong, so score is 1 to 1"

kleiba 7mo ago
Thanks again - this time I have to admit I really don't get what you're trying to say?!
- refulgentis 7mo ago
  Sorry, I was unclear! You said you wished someone with Lean knowledge could check my work. I'm saying: you can check it yourself, right now, without knowing Lean. Click any of links [2] through [5]. You'll see the word `axiom` in the code. In Lean, `axiom` means "assume this is true without proof." That's it. That's the whole critique. The paper says "formally verified," but the key claims — FFN computes Bayesian update, attention routes correctly, BP converges, no hallucination — are all just assumed. You don't need to take my word for it, and you don't need a Lean expert to break a tie. The evidence is right there in the links. It'd be like a paper claiming "we formally proved this bridge is safe" and the proof says "Axiom: this bridge is safe." You don't need a civil engineer to tell you that's not a proof.