7 ms·

Mine took 20min. Pro. https://chatgpt.com/share/69ed83b1-3704-8322-bcf2-322aa85d7a99 https://chatgpt.com/share/69ed83b1-3704-8322-bcf2-322aa85d7a... But I wish

Mine took 20min. Pro. https://chatgpt.com/share/69ed83b1-3704-8322-bcf2-322aa85d7a99 https://chatgpt.com/share/69ed83b1-3704-8322-bcf2-322aa85d7a... But I wish I was math smart to know if it worked or not.

vjerancrnjak 6mo ago
Ask it to formalize it in Lean.
- dbdr 6mo ago
  That's great if it works. But it's way harder to produce a formal proof. So my expectation is that this will fail for most difficult problems, even when the non-formal proof is correct.
- utopiah 6mo ago
  If they aren't "smart enough" to know if it work they most likely are also unable to verify if the Lean formalization is indeed the one that matches the problem they were trying to solve.
  - timjver 6mo ago
    Verifying that every step in a (potentially long) proof is sound can of course be much, much harder than verifying that a definition is correct. That's kind of the whole point.
    - LeCompteSftware 6mo ago
      That's not what the parent comment meant. They meant checking the Lean-language definitions actually match the mathematical English ones, and that the Lean theorems match the ones in the paper. If that's true then you don't actually need to check the proofs. But you absolutely need to check the definitions, and you can't really do that without sufficient mathematical maturity.
      - smallnamespace 6mo ago
        Yes, and the child comment’s point is that formalizing the problem is likely easier than having the LLM verify that each step of a long deduction is correct, which is why Lean might be helpful.
        LeCompteSftware 6mo ago
        But both of you are ignoring the parent comment! Actually you're ignoring the context of the thread. Originally someone said "I wish I was math smart to know if [this vibe-mathematics proof] worked or not." They did NOT say "I'd like to check but I am too lazy." Suggesting "ask it to formalize it in Lean" is useless if you're not mathematically mature enough to understand the proof, since that means you're not mathematically mature enough to understand how to formalize the problem. Then "likely easier" is a moot point. A Lean program you're not knowledgeable enough to sanity-check is precisely as useless as a math proof you're not knowledgeable enough to read.
        utopiah 6mo ago
        thanks
        smallnamespace 6mo ago
        It’s not useless, because you can, for example, ask multiple frontier models to do the formalization and see if they agree. And if they have surface-level differences in formalization, you can also ask them whether apparently-different definitions are equivalent. This isn’t perfect of course - perhaps every single model is wrong. But you are too quick to declare that something isn’t useful for arriving at an answer. Reducing the surface area of what needs to be checked is good regardless.
- DonHopkins 6mo ago
  Formalize this in the form of a Iranian Lego Trump Dis Rap video.
liweic 6mo ago
Wired enough, Pro+extended with the same prompt, just output directly without thinking: https://chatgpt.com/s/t_69edd2d9dc048191b1476db92c0dedf8 https://chatgpt.com/s/t_69edd2d9dc048191b1476db92c0dedf8 . Does this mean the result was cached or that it simply routes to a different model silently based on the user?
- Vachyas 6mo ago
  The link you provided is for a canvas I think rather than the convo

vjerancrnjak 6mo ago

Ask it to formalize it in Lean.

dbdr 6mo ago
That's great if it works. But it's way harder to produce a formal proof. So my expectation is that this will fail for most difficult problems, even when the non-formal proof is correct.
utopiah 6mo ago
If they aren't "smart enough" to know if it work they most likely are also unable to verify if the Lean formalization is indeed the one that matches the problem they were trying to solve.
- timjver 6mo ago
  Verifying that every step in a (potentially long) proof is sound can of course be much, much harder than verifying that a definition is correct. That's kind of the whole point.
  - LeCompteSftware 6mo ago
    That's not what the parent comment meant. They meant checking the Lean-language definitions actually match the mathematical English ones, and that the Lean theorems match the ones in the paper. If that's true then you don't actually need to check the proofs. But you absolutely need to check the definitions, and you can't really do that without sufficient mathematical maturity.
    - smallnamespace 6mo ago
      Yes, and the child comment’s point is that formalizing the problem is likely easier than having the LLM verify that each step of a long deduction is correct, which is why Lean might be helpful.
      - LeCompteSftware 6mo ago
        But both of you are ignoring the parent comment! Actually you're ignoring the context of the thread. Originally someone said "I wish I was math smart to know if [this vibe-mathematics proof] worked or not." They did NOT say "I'd like to check but I am too lazy." Suggesting "ask it to formalize it in Lean" is useless if you're not mathematically mature enough to understand the proof, since that means you're not mathematically mature enough to understand how to formalize the problem. Then "likely easier" is a moot point. A Lean program you're not knowledgeable enough to sanity-check is precisely as useless as a math proof you're not knowledgeable enough to read.
        utopiah 6mo ago
        thanks
        smallnamespace 6mo ago
        It’s not useless, because you can, for example, ask multiple frontier models to do the formalization and see if they agree. And if they have surface-level differences in formalization, you can also ask them whether apparently-different definitions are equivalent. This isn’t perfect of course - perhaps every single model is wrong. But you are too quick to declare that something isn’t useful for arriving at an answer. Reducing the surface area of what needs to be checked is good regardless.
DonHopkins 6mo ago
Formalize this in the form of a Iranian Lego Trump Dis Rap video.

liweic 6mo ago

Wired enough, Pro+extended with the same prompt, just output directly without thinking: https://chatgpt.com/s/t_69edd2d9dc048191b1476db92c0dedf8 https://chatgpt.com/s/t_69edd2d9dc048191b1476db92c0dedf8 . Does this mean the result was cached or that it simply routes to a different model silently based on the user?

Vachyas 6mo ago
The link you provided is for a canvas I think rather than the convo