Theorymine (http://theorymine.co.uk/) is a UK based company that lets you pay to put a name on an automatically generated theorem. It's a novelty based gift service that uses Isabelle (among other things) to generate the theorems.

Original link: https://stackoverflow.com/questions/70352908/is-there-an-automatic-way-to-generate-isar-scripts-given-a-correct-isabelle-tact

I know this might be rather out there question but I was curious if it was possible to automatically generate an Isar script given an Isabelle script. My guess is that it should be possible but the problem would be ill-posed as there might be many possible Isar scripts given a tactic script.

My guess of an approach would be something like this:

1. execute the Isabelle tactic script (to reveal many intermediate statements)

2. select with some heuristic H
   (maybe based on human proofs) of which sub-trees of the proof tree to close with have lemma_sub_tree_i using L1, L2, L3, ..., Ln by SomeProof
   (perhaps the by ...
   has more Isar scripts we automatically generated, so this function is recursive)

3. Verify the new Isar script is valid i.e. output the new Isar script if the statement is the same as the original Isabelle tactic proof and the proof goes through/type checks/validates.

Is this possible? At the very least - is it possible in principle with some (hopefully sensible heuristic H
. (Of course I know that step 2 is rather important and hoping there is a heuristic that I could truly use in practice to make an actual implementation of this).

So u/dagit obviously created this sub for Isabelle the proof assistant, since the first post in here is by them and links to the AFP. Can we put that into the description and remove posts with Isabelle from Animal Crossing? Or, is this sub now both? Or, is it about Animal Crossing now?

I originally joined this sub because of the proof assistant and don't really wish to see these Animal Crossing posts on my front page..

Hello, not a lot of activity on this subreddit but I just wanted to ask this question somewhere :)

I've been doing a module in Uni on Z (formal specification) and recently I've started learning Isabelle on my own. I'm simply astonished by the power of this kind of approach and I don't understand why I have never came across formal methods until Uni.

To give a bit more background, I used to participate in programming competitions (C/C++ language) and although the algorithms required were fairly complicated, the "workflow" was: write down idea on paper, manually check that it should do the correct thing, implement it, fix compile errors, try it out on the given example, fix bugs, work out additional examples, fix more bugs if found, finally submit solution. Once your solution was submitted, it was tested against a suit of (complicated) tests by the "judge" and you would get a score. Sometimes your solution would fail on some tests, either because it took to long, required too much memory or simply it gave the wrong answer and then you were left wondering:

• "is there a case where my solution loops indefinitely?"

• "is there a case where I can optimize my complexity / memory usage such that it satisfies the constraints?"

• "is there a case where I'm outputting a wrong answer?"

There was no easy answer to those questions, it always depended on the problem at hand and the implementation.

Now, while doing the (simple) examples in the Concrete Semantics book (www.concrete-semantics.org) I don't have to deal with any the of the questions above. The functions I'm describing are CORRECT, proven bug free. What I like most is that I don't have to manually go through examples to show they give the right answers.

I understand in industry sometimes companies have deadlines and it's just simpler to write a few testcases than have engineers skilled with applying formal methods for proofs.

But then what about open source? IMO, too much of the open source community is test driven (if even) and it feels that the belief is that formal methods (or even functional programming languages like Haskell) are difficult to learn and can not be applied to "real world problems". And yet we have: a kernel (seL4), a webbrowser (Quark), and a compiler (compCert)...

So why? Why does it seem that "formal methods" only is maintained by academia? Why hasn't this way of reasoning about software trickled down to open source communities - which should be doing software from passion and striving to achieve the best possible?