It's the same overall project, but that result uses kissat[1] solver to complete the solve, this update is that we made our own kissat-style solver specifically for SHA-256. (As of the yesterday's post, I only said "we are working on our own version of the kissat solver based on these properties"[2]). Now we have that solver. It's exciting because we have a large body of Lean-proven theorems, many novel, and we think we can apply many of them directly in this sat solver. Of course, we could be going down a path that doesn't lead to a collision, as we did when we tried to extend the reduced-round records using a mini neural network.[3] We'll just have to see if we can extend the results at all.
OP, 23 days ago: https://news.ycombinator.com/item?id=47263574
If you "don't know what [claude] is doing" then you should not "trust it when it says it made a fundamental discovery".
Thanks for your feedback, I'll keep it in mind.
You posted about it yesterday (61 points, 75 comments) https://news.ycombinator.com/item?id=47546028
It's the same overall project, but that result uses kissat[1] solver to complete the solve, this update is that we made our own kissat-style solver specifically for SHA-256. (As of the yesterday's post, I only said "we are working on our own version of the kissat solver based on these properties"[2]). Now we have that solver. It's exciting because we have a large body of Lean-proven theorems, many novel, and we think we can apply many of them directly in this sat solver. Of course, we could be going down a path that doesn't lead to a collision, as we did when we tried to extend the reduced-round records using a mini neural network.[3] We'll just have to see if we can extend the results at all.
[1] https://github.com/arminbiere/kissat
[2] https://stateofutopia.com/papers/2/we-broke-92-percent-of-sh...
[3] https://news.ycombinator.com/item?id=47554283