[predictsoft]

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

[soloist11]

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.

[bubblyworld]

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

[tobinfricke]

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.

[bubblyworld]

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

[fragmede]

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...