3 ms·

The concept of reachability is pretty interesting in general as well. "Can a spaceship with a certain delta-v reach another planet within an n-body system? (An

The concept of reachability is pretty interesting in general as well. "Can a spaceship with a certain delta-v reach another planet within an n-body system? (And if so, what is the fastest-to target/most resource preserving acceleration schedule?)" - apparently necessitates brute force, practically not computable on long time scales due to the chaos inherent in n-body systems (https://space.stackexchange.com/questions/64392/escaping-earth-how-could-one-attempt-to-find-the-best-solution-to-this-traject https://space.stackexchange.com/questions/64392/escaping-ear..., https://en.wikipedia.org/wiki/N-body_problem https://en.wikipedia.org/wiki/N-body_problem) "Can a math proof be reached (within a certain number of proof steps) from the axioms?" - equivalent to the halting problem in most practical systems (https://math.stackexchange.com/questions/3477810/estimating-meta-mathematical-properties-of-conjectures https://math.stackexchange.com/questions/3477810/estimating-...) "Can a demoscene program with a very limited program size visualize (or codegolf program output) something specific?" - asking for nontrivial properties like this usually requires actually running each program, and there are unfathomably many short programs (https://www.dwitter.net/ https://www.dwitter.net/ is a good example of this) "In cookie-clicker games, is it possible to go above a certain score within a certain number of game ticks using some sequence of actions?" - in all but the simplest and shortest games (like https://qewasd.com https://qewasd.com), this is at least not efficiently (optimally) solvable using MILP and the like, as the number of possible action sequences increases exponentially And yet, despite these being really hard (or in the general case, impossible) problems, humans use some heuristics to achieve progress

westurner 3y ago
Quantum Discord: https://en.wikipedia.org/wiki/Quantum_discord https://en.wikipedia.org/wiki/Quantum_discord Quantum nonlocality: https://en.wikipedia.org/wiki/Quantum_nonlocality https://en.wikipedia.org/wiki/Quantum_nonlocality Butterfly effect -> Quantum chaos: https://en.wikipedia.org/wiki/Quantum_chaos https://en.wikipedia.org/wiki/Quantum_chaos -> Perturbation theory: https://en.wikipedia.org/wiki/Perturbation_theory_(quantum_mechanics) https://en.wikipedia.org/wiki/Perturbation_theory_(quantum_m... But then entropy in fluids, Satisfiability > Model Theory: https://en.wikipedia.org/wiki/Satisfiability https://en.wikipedia.org/wiki/Satisfiability Goal programming: https://en.wikipedia.org/wiki/Goal_programming https://en.wikipedia.org/wiki/Goal_programming And, ultimately, Self play (AlphaZero, ) https://en.wikipedia.org/wiki/Self-play https://en.wikipedia.org/wiki/Self-play "Q: LLM and/or an RL agent trained on [Lean mathlib] and tests" https://github.com/leanprover-community/mathlib/issues/17919 https://github.com/leanprover-community/mathlib/issues/17919
sudosysgen 3y ago
>"Can a demoscene program with a very limited program size visualize (or codegolf program output) something specific?" - asking for nontrivial properties like this usually requires actually running each program, and there are unfathomably many short programs (https://www.dwitter.net/ https://www.dwitter.net/ is a good example of this) This is equivalent to computing the Kolmogorov complexity of the desired output, which is uncomputable - you can pretty easily show that solving this implies solving the Halting Problem.
- eru 3y ago
  That's for the general case. If the program size limit is generous enough and/or the required thing to visualize is simple enough, you might be able to give the Yes answer easily without running into any major trouble. The No answer is harder.
PeterisP 3y ago
Generally, for these tasks when we say "humans can solve them" then people are not solving the same problem; they're trying (and succeeding) to find a good solution (where various heuristics work), and often for most, realistic cases only, while the theoretical problem is to have a process that will certainly find a solution that's guaranteed to be the absolute best possible even in weird degenerate cases, and that simply is a very different, much harder problem. E.g. halting problem, traveling salesman, etc, etc have people commenting that "but humans can solve them" in this manner.
Someone 3y ago
> And yet, despite these being really hard (or in the general case, impossible) problems, humans use some heuristics to achieve progress. That’s because, in many of these problems, the theoretically hard cases are rarely encountered in practice.
schoen 3y ago
> "Can a math proof be reached (within a certain number of proof steps) from the axioms?" - equivalent to the halting problem in most practical systems (https://math.stackexchange.com/questions/3477810/estimating- https://math.stackexchange.com/questions/3477810/estimating-...) The answer that observed this was equivalent to the Halting Problem wasn't keeping the "within a certain number of proof steps" constraint there, but referring to the question of whether an arbitrary proposition was provable or not provable. If you do specify a number of steps in advance, I don't think the problem is solvable faster than brute force in general, but all individual instances can be decided at least by brute force. In fact, there are tactics in computer proof systems where you specify a search depth, and the tactic can tell you whether or not there is a valid proof (using certain rules of inference, which probably won't be all the rules of inference allowed by the system!) closer to your current hypotheses than that depth. This is like the distinction between Gödel's last two definitions in his long chain of definitions in "On Formally Undecidable Propositions": > 45. x B y ≡ Bw(x) & [l(x)] Gl x = y > x is a proof of the formula y. > 46. Bew(x) ≡ (E y) y B x > x is a provable formula. [Bew(x) is the only one of the concepts 1-46 of which it cannot be asserted that it is recursive.] Here Gödel notes that all of his previous definitions that used existential quantifiers set an explicit limit for the size of the integer in question (there exists k such that k is less than or equal to ...), but definition 46 doesn't: it just says "there exists an integer y such that y is a proof of x" (according to Gödel numbering). If you did set a limit on the size of y then you would have a computable function, where the most naive implementation would be to just evaluate everything up to that size limit and check whether it is a valid proof of x (using Gödel's other formulas such as Bw). But it wouldn't match our overall notion of provability, because our notion of provability doesn't set any particular limit on the size of the proof.
- eru 3y ago
  > If you do specify a number of steps in advance, I don't think the problem is solvable faster than brute force in general, but all individual instances can be decided at least by brute force. For systems where you can check a given proof in polynomial time, this problem becomes 'merely' NP-complete. (Technically, the maximum size of the proof you are willing to accept needs to be a polynomial in the length of the statement you are trying to prove.)
eru 3y ago
> And yet, despite these being really hard (or in the general case, impossible) problems, humans use some heuristics to achieve progress Computers can also use heuristics to achieve progress (in many cases).

westurner 3y ago

Quantum Discord: https://en.wikipedia.org/wiki/Quantum_discord https://en.wikipedia.org/wiki/Quantum_discord Quantum nonlocality: https://en.wikipedia.org/wiki/Quantum_nonlocality https://en.wikipedia.org/wiki/Quantum_nonlocality Butterfly effect -> Quantum chaos: https://en.wikipedia.org/wiki/Quantum_chaos https://en.wikipedia.org/wiki/Quantum_chaos -> Perturbation theory: https://en.wikipedia.org/wiki/Perturbation_theory_(quantum_mechanics) https://en.wikipedia.org/wiki/Perturbation_theory_(quantum_m... But then entropy in fluids, Satisfiability > Model Theory: https://en.wikipedia.org/wiki/Satisfiability https://en.wikipedia.org/wiki/Satisfiability Goal programming: https://en.wikipedia.org/wiki/Goal_programming https://en.wikipedia.org/wiki/Goal_programming And, ultimately, Self play (AlphaZero, ) https://en.wikipedia.org/wiki/Self-play https://en.wikipedia.org/wiki/Self-play "Q: LLM and/or an RL agent trained on [Lean mathlib] and tests" https://github.com/leanprover-community/mathlib/issues/17919 https://github.com/leanprover-community/mathlib/issues/17919

sudosysgen 3y ago

>"Can a demoscene program with a very limited program size visualize (or codegolf program output) something specific?" - asking for nontrivial properties like this usually requires actually running each program, and there are unfathomably many short programs (https://www.dwitter.net/ https://www.dwitter.net/ is a good example of this) This is equivalent to computing the Kolmogorov complexity of the desired output, which is uncomputable - you can pretty easily show that solving this implies solving the Halting Problem.

eru 3y ago
That's for the general case. If the program size limit is generous enough and/or the required thing to visualize is simple enough, you might be able to give the Yes answer easily without running into any major trouble. The No answer is harder.

PeterisP 3y ago

Generally, for these tasks when we say "humans can solve them" then people are not solving the same problem; they're trying (and succeeding) to find a good solution (where various heuristics work), and often for most, realistic cases only, while the theoretical problem is to have a process that will certainly find a solution that's guaranteed to be the absolute best possible even in weird degenerate cases, and that simply is a very different, much harder problem. E.g. halting problem, traveling salesman, etc, etc have people commenting that "but humans can solve them" in this manner.

Someone 3y ago

> And yet, despite these being really hard (or in the general case, impossible) problems, humans use some heuristics to achieve progress. That’s because, in many of these problems, the theoretically hard cases are rarely encountered in practice.

schoen 3y ago

> "Can a math proof be reached (within a certain number of proof steps) from the axioms?" - equivalent to the halting problem in most practical systems (https://math.stackexchange.com/questions/3477810/estimating- https://math.stackexchange.com/questions/3477810/estimating-...) The answer that observed this was equivalent to the Halting Problem wasn't keeping the "within a certain number of proof steps" constraint there, but referring to the question of whether an arbitrary proposition was provable or not provable. If you do specify a number of steps in advance, I don't think the problem is solvable faster than brute force in general, but all individual instances can be decided at least by brute force. In fact, there are tactics in computer proof systems where you specify a search depth, and the tactic can tell you whether or not there is a valid proof (using certain rules of inference, which probably won't be all the rules of inference allowed by the system!) closer to your current hypotheses than that depth. This is like the distinction between Gödel's last two definitions in his long chain of definitions in "On Formally Undecidable Propositions": > 45. x B y ≡ Bw(x) & [l(x)] Gl x = y > x is a proof of the formula y. > 46. Bew(x) ≡ (E y) y B x > x is a provable formula. [Bew(x) is the only one of the concepts 1-46 of which it cannot be asserted that it is recursive.] Here Gödel notes that all of his previous definitions that used existential quantifiers set an explicit limit for the size of the integer in question (there exists k such that k is less than or equal to ...), but definition 46 doesn't: it just says "there exists an integer y such that y is a proof of x" (according to Gödel numbering). If you did set a limit on the size of y then you would have a computable function, where the most naive implementation would be to just evaluate everything up to that size limit and check whether it is a valid proof of x (using Gödel's other formulas such as Bw). But it wouldn't match our overall notion of provability, because our notion of provability doesn't set any particular limit on the size of the proof.

eru 3y ago
> If you do specify a number of steps in advance, I don't think the problem is solvable faster than brute force in general, but all individual instances can be decided at least by brute force. For systems where you can check a given proof in polynomial time, this problem becomes 'merely' NP-complete. (Technically, the maximum size of the proof you are willing to accept needs to be a polynomial in the length of the statement you are trying to prove.)

eru 3y ago

> And yet, despite these being really hard (or in the general case, impossible) problems, humans use some heuristics to achieve progress Computers can also use heuristics to achieve progress (in many cases).