3 ms·
Wouldn't that be the point of pairing it with Lean? You wouldn't get false positives.
by generalizations 3y ago
Wouldn't that be the point of pairing it with Lean? You wouldn't get false positives.
- Sharlin 3y agoDoesn’t mean you’d get true positives either. Garbage in, garbage out.
- akoboldfrying 3y agoIIUC, any sensible way of "pairing up" these things will mean that anything you get out will be true. But the search might take millennia, and the outcome might be nothing (equivalently, "the LLM's conjecture is false").
- hackerlight 3y agoThis is equivalent to saying it's not going to work.