* First, it's written in the typical style of AI slop.
* Second, a mathematician I know and trust writes "I went straight to the technical part (Sect. 3) and randomly checked one of the results (Theorem 3.14), finding that it is obviously false. (The category Comp mentioned in the theorem is formally introduced and makes sense per se, but it is certainly not additive with the proposed definition, as claimed in the statement of the theorem)."
* Third, another mathematician I know and trust writes "I spent almost an hour poking through here carefully to see where the more central claims begin to fall apart. Theorems 3.24 and 4.1 brazenly contradict each other, proving respectively that problems in P are homologically trivial and that all NP-complete problems are homologically isomorphic to all problems in NP. Even more to the point, the proof of 3.24 really shows the lie where it says "The detailed argument uses the functoriality of the computational homology construction and the fact that homology isomorphisms preserve the 'computational topology' of problems." The last claim is, naturally, not mathematically defined. The computational chain complex also appears not to be genuinely defined, as far as I can tell. I haven't compared to see what the author chucked into the formalized definition."
Every time I try to understand algebraic geometry I get stuck at just beyond varieties and ideals. I can't even work my way up to chain complexes and homologies to even get a hold on the content. Honestly functors and natural transformations, I dont grok either, so its greek to me.
Like whenever i'm working through definitions or content it all makes sense. But not being a working mathematician it all just blurs away into abstract nonsense that I can't organize internally.
Learning homological algebra is a long way away from learning about varieties and ideals in any sensible order in which to learn material. You have to do a lot of work in between in order for homological algebra to seem motivated. Sounds like you ought to try an introduction to algebraic topology.
Is this LLM-generated? The style is somewhat off (long lists repeating the same thing over and over, calling random meta statements “theorems”), and the link to the repo is completely broken.
Yes. From a quick scan of the paper, it includes a formal proof in Lean4. That said, it is very long and complicated, with lots of steps in the chain (as you might expect) so it would need to be checked carefully to ensure it proves what it claims to prove.
Lean uses Curry-Howard correspondence, so how proofs work is you declare your propositions as types and then your proof is actually a recipe that goes from things that have already been established and finishes by instantiating that type. The guarantees there are very strong - if you succeed in instantiating the type you have definitely proved something. The question is whether you have proved the thing you said you have. So here scanning the proof (it’s like 100 pages and I am sick so definitely sub-par intellectually) they use category theory to embed the problem, so the proof is actually a proof of the properties of this embedding. So if there is a problem with the proof, my guess would be that it would lie in the embedding not being exactly representative of the problem somehow.
It seems a pretty serious attempt though- it’s not just some random crank paper.
math looks pretty legit. the only issue would come from the formulation of the category Comp and if it actually represents what it wants to. Hopefully some bigshot looks at this soon
johncarlosbaez|4 months ago
* First, it's written in the typical style of AI slop.
* Second, a mathematician I know and trust writes "I went straight to the technical part (Sect. 3) and randomly checked one of the results (Theorem 3.14), finding that it is obviously false. (The category Comp mentioned in the theorem is formally introduced and makes sense per se, but it is certainly not additive with the proposed definition, as claimed in the statement of the theorem)."
* Third, another mathematician I know and trust writes "I spent almost an hour poking through here carefully to see where the more central claims begin to fall apart. Theorems 3.24 and 4.1 brazenly contradict each other, proving respectively that problems in P are homologically trivial and that all NP-complete problems are homologically isomorphic to all problems in NP. Even more to the point, the proof of 3.24 really shows the lie where it says "The detailed argument uses the functoriality of the computational homology construction and the fact that homology isomorphisms preserve the 'computational topology' of problems." The last claim is, naturally, not mathematically defined. The computational chain complex also appears not to be genuinely defined, as far as I can tell. I haven't compared to see what the author chucked into the formalized definition."
emtel|4 months ago
soup10|4 months ago
quamserena|4 months ago
https://github.com/comphomology/pvsnp-formal
steego|4 months ago
Who writes Lean code in the actual paper but doesn't create a repo or even a username?
nh23423fefe|4 months ago
Like whenever i'm working through definitions or content it all makes sense. But not being a working mathematician it all just blurs away into abstract nonsense that I can't organize internally.
johncarlosbaez|4 months ago
* Karen E. Smith, Lauri Kahanpää, Pekka Kekäläinen and William Traves, An Invitation to Algebraic Geometry, Springer, Berlin, 2004.
and then this:
* Igor R. Shafarevich, Basic Algebraic Geometry, two volumes, third edition, Springer, 2013.
orangea|4 months ago
goldsteinq|4 months ago
rescrv|4 months ago
seanhunter|4 months ago
Lean uses Curry-Howard correspondence, so how proofs work is you declare your propositions as types and then your proof is actually a recipe that goes from things that have already been established and finishes by instantiating that type. The guarantees there are very strong - if you succeed in instantiating the type you have definitely proved something. The question is whether you have proved the thing you said you have. So here scanning the proof (it’s like 100 pages and I am sick so definitely sub-par intellectually) they use category theory to embed the problem, so the proof is actually a proof of the properties of this embedding. So if there is a problem with the proof, my guess would be that it would lie in the embedding not being exactly representative of the problem somehow.
It seems a pretty serious attempt though- it’s not just some random crank paper.
krackers|4 months ago
beanshadow|4 months ago
https://github.com/comphomology/pvsnp-formal
il_abi|4 months ago
yyyk|4 months ago
https://www.reddit.com/r/computerscience/comments/1odgx6v/le...
https://www.reddit.com/r/learnmath/comments/1odh3f5/is_this_...