3 ms·
Are there any suggesters built on top of these proof assistants that have been suggested recently? Like code completion engines but for proofs?
by worldsayshi 4y ago
Are there any suggesters built on top of these proof assistants that have been suggested recently? Like code completion engines but for proofs?
- worldsayshi 4y agoAlso, has anyone tried building a puzzle game using a proof assistant?
- gmfawcett 4y agoI'm pretty sure that Coq is a puzzle game itself, masquerading as a proof assistant!
- schoen 4y agoI've used Z3 to create some logic puzzles, but I was using the SAT solver features rather than the proof features. One effective, if naive, approach to determining whether a logic puzzle has a unique solution is checking: * is my current constraint set satisfiable? * if so, exhibit a satisfying assignment ("foo") * add a new constraint that explicitly excludes the solution "foo" * is the resulting constraint set satisfiable? * if not, great! (the solution "foo" is unique)
- abecedarius 4y agohttps://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... You could go further towards it feeling like a game, yes -- I've been wanting that too. I'm still learning the basics of these things.
- schoen 4y agoBefore playing the Natural Number Game, I played the Incredible Proof Machine: http://incredible.pm/ http://incredible.pm/ It's fun! Admittedly the diagrams tend to explode in size for complicated proofs.
- zaik 4y agoLike this? https://coq-tactician.github.io/ https://coq-tactician.github.io/
- worldsayshi 4y agoInteresting! Although I realize I might actually be looking for a SAT solver suggester than what I said.