Hacker News Reader

Comment by predictsoft | Hacker News Reader

I just asked ChatGPT that and it seemed to come up with a good answer.

Now ask it to convert the computation into a logical calculus so that it can be verified with a theorem prover like Coq, Lean, or Isabelle.

What are you actually getting at with this? Formalising algebraic topology in Lean is still _very_ much an open project, for instance.

You'd think with all those billions spent on the software and the hardware it would be a walk in the park to convert a single book on algebraic topology into a formalized Coq, Lean, or Isabelle module. Seems like a very obvious test case for the intelligence capabilities of these systems. I know that it is possible because Kevin Buzzard is going to formalize Fermat's last theorem for less than £934,043 but no commercial AI lab has yet managed to build an AI that can do basic arithmetic. [0] Mira Murati is on the record about their next AI model and that it will have the intelligence of a PhD student so let's see if their next model can actually formalize basic algebraic topology into a logical calculus. [1]

0: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y0...

1: https://engineering.dartmouth.edu/news/openai-cto-mira-murat...

Why would you think that's a walk in the park? Have you actually tried formalising stuff in Lean/Coq? I have, and even with a postgraduate maths degree behind me it's hard as hell!

The fact that Kevin and his team are formalising FLT is incredible, but they all have decades of experience with this stuff (!!).

Transformers can do arithmetic (and many other things) just fine, do a bit of searching on arxiv and you'll find papers from 2023 showing that nano-scale transformer models suffice. It really is a data problem, not a fundamental limitation with the technology.

What is your degree in?

Master's studying representation theorems in nonmonotonic logic, left academia for industry during my PhD. Fun spaced out maths problems. I tried to formalize my thesis in Lean but it is nowhere near as simple as you make it out to be.

You are really onto something here. LLMs aren't really perfect. Good catch.

Perfection is not the problem. An obvious test case of intelligence is to formally model something like algebraic topology in a formal logical calculus like intensional type theory with identity types. Even though all the commercial labs have ingested all of nLab, there isn't a single commercial model that can use logic to perform arithmetic operations.

OK, so it seems you didn't get the memo: LLMs at the present stage have not yet reached AGI, and have some notable other flaws, like not being able to do math reliably. Commercial interests will try to exaggerate the current capabilities, but most people can see through that.

The capabilities are nonetheless nothing short of astounding, given where we were 10 or even 2 years ago, and clearly point to a near future where we can expect the machines overcome these shortcomings.

Thousands, if not millions, of researchers, coders and others will have to adjust their worklife expectations, just like previous technological revolutions have seen thousands of other professions disappear into think air.

Sure, good luck with this AGI business. I'm sure it will work out great for everyone in the end.

The output of ChatGPT almost always sounds good. That's the point.

But I would wager that its answer was at least wrong, and perhaps total nonsense.

That's the real hazard of using ChatGPT as a learning tool. You are in no position to evaluate whether the output makes any sense.

I asked it to compute the simplicial homology of RP^2 and not only was it spot on with the result, it gave me a detailed and essentially correct computation. This definitely appears in its training set, but nevertheless you should have some humility =P

How do you know it's correct? The only simplicial traingulation I know of is by splitting up the sphere into an icosahedron and then identifying all the opposite faces to get the proper antipodal action for the quotient.

I'm not interested in engaging with you further on this topic after you devolved into ad hominems against me in the other thread. I'm here to argue in good faith. Have a good day.

You made an incorrect assessment of a basic calculation in algebraic topology and claimed that it was correct. You didn't even look at what it was computing and simply looked at the final answer which lined up with the answer on Wikipedia. Simplicial calculations for projective planes are not simple. The usual calculations are done with cellular decomposition and that's why the LLM gives the wrong answer, the actual answer is not in the dataset and requires reasoning.

Are you confusing me with someone else? When I asked it GPT computed the homology from the CW decomposition of RP^2 with three cells. Which is a very simple exercise.

I recommend that you give it a try.

That's ok. It seems like LLMs know all about simplicial complexes and homology so I'll spend my time on more fruitful endeavors but thanks for the advice.

To be fair, it's not a simplicial complex, but simplicial and cellular homology coincide on triangulatable spaces like RP^2 so I gave it the benefit of the doubt =) algebraic topology is a pretty fun field regardless of how much a language model knows about it IMO.

Do you have a reference for this equivalency?

It's in Hatcher iirc

I dunno what you wanted to wager, but I would still be interested in the holes in this answer.

https://chatgpt.com/share/e84800dd-c714-42d4-977b-b446c5c5ed...

That's incorrect.

No it isn't.

lmao. you're totally right. RP^2 can be triangulated with a single triangle with all of its vertices identified. that's totally how you compute the simplicial decomposition of RP^2

I asked you explain why it's wrong, and all you said was "that's incorrect". Saying "no it isn't" got you to explain your answer far better than how I directly asked you to in the first place.

Don't worry, we'll have AGI soon and it will give the correct answer instead of whatever plausible nonsense it put together this time. I have faith.

Reply on news.ycombinator.com