← Back to context Comment by philipfweiss 5 hours ago Maybe consider an integration with theoremdb.org? 3 comments philipfweiss Reply fractorial 4 hours ago To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.Value is in how maths is communicated: The process, frustrations, triumphs, etc.We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them. andxor 2 hours ago > hooking up slop to slop is just unlikely to produce anything valuableDo you have a formal proof of that? skew-aberration 28 minutes ago Premises: Garbage in implies garbage out (first principle of computer science) The input is possibly, but not necessarily garbage (definition of slop)By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
fractorial 4 hours ago To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.Value is in how maths is communicated: The process, frustrations, triumphs, etc.We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them. andxor 2 hours ago > hooking up slop to slop is just unlikely to produce anything valuableDo you have a formal proof of that? skew-aberration 28 minutes ago Premises: Garbage in implies garbage out (first principle of computer science) The input is possibly, but not necessarily garbage (definition of slop)By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
andxor 2 hours ago > hooking up slop to slop is just unlikely to produce anything valuableDo you have a formal proof of that? skew-aberration 28 minutes ago Premises: Garbage in implies garbage out (first principle of computer science) The input is possibly, but not necessarily garbage (definition of slop)By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
skew-aberration 28 minutes ago Premises: Garbage in implies garbage out (first principle of computer science) The input is possibly, but not necessarily garbage (definition of slop)By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.
To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.
Value is in how maths is communicated: The process, frustrations, triumphs, etc.
We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them.
> hooking up slop to slop is just unlikely to produce anything valuable
Do you have a formal proof of that?
Premises: Garbage in implies garbage out (first principle of computer science) The input is possibly, but not necessarily garbage (definition of slop)
By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.