Search with q#, constraints through z3

Stream: Equational

[Michael Bucko]

I posted this: https://github.com/riccitensor/quantummath

Don't have much experience with quantum algorithms (but have been reading a lot). Will try to connect the z3 code (esp. the one related to the 1485 research) with:

• Q# - it's not clear yet how to do this exactly
• Lean - also not clear / I guess that'd have to start very small, maybe with just finding an operation table
• Curriculum learning - there'd be lineage, progress, etc.
• Egg - for equivalent program storage
• TPTP - or should it be a different format? what's the SOTA here?

Does it make sense? What's your feedback? Do you see any problems with this approach?

Should I port the existing z3 code to Rust?

[Michael Bucko]

This starts very small, with the 5 "manaces" (broken down into those two groups based on @Terence Tao 's insights from his wiki blog):

• 1323, 1516, 1729
• 1485, 854

Hopefully, at least one of them will be defeated with next-gen approach to ATP.

It could also be that we won't beat them that easily..

[Daniel Weber]

Is there any viability to using quantum algorithms here? I don't think quantum computers large enough to be useful here exist yet

[Michael Bucko]

Daniel Weber schrieb:

Is there any viability to using quantum algorithms here? I don't think quantum computers which are large enough to be useful here exist yet

For me, it's a learning experiment. What I see is that is that specific subtasks could be perhaps parallelized, but I am trying to do it the new way, rather than Spark / TFD.
Another option is to, for instance, do the cuML/RAPIDS, or K8s + Vertex.

[Michael Bucko]

I used to test some small q scripts back in the day, but - assuming we can make this run in a couple of days - we could ask some of the big players for access to a quantum computer.

[Jose Brox]

Daniel Weber ha dicho:

Is there any viability to using quantum algorithms here? I don't think quantum computers large enough to be useful here exist yet

If the problem to solve can be written as an optimization problem, then it can be subject to quantum annealing, for which there already are quantum computers (like those of the D-Wave company) because the connection needed between qubits is not that strong.

Nevertheless, I don't think we are having dificulties with computing power, for this project I tend to believe that when we don't find a proof in a sensible time it is because none exists.

[Michael Bucko]

Jose Brox schrieb:

Nevertheless, I don't think we are having dificulties with computing power, for this project I tend to believe that when we don't find a proof in a sensible time it is because none exists.

Maybe they really don't exist, but I'm having lots of compute issues every day (because of the work I usually do). Everything seems to be running forever, and "GPU poor" is really the reality.

Nonetheless, I understand this is not immediately useful. Just wanted to share this with you. I'll be sharing some code here too in the future.

[Amir Livne Bar-on]

If there's a way to get a random magma obeying some law it'd be amazing (for the laws where finite counter-examples are relevant)

[Michael Bucko]

Amir Livne Bar-on [schrieb]

If there's a way to get a random magma obeying some law it'd be amazing (for the laws where finite counter-examples are relevant)

I'll experiment with z3 and get back to you.