Jason (jcreed) wrote,
Jason
jcreed

A list of 100 theorems indicating which of them have been formally verified. Even though the list is of course rather arbitrary, I think this is a neat thing, inasmuch as benchmarks are better than nothing.

---

And if anyone finds themselves on cygwin and trying to follow the HOL Light tutorial, bear in mind you may need to follow the advice here and run ocamlmktop -o ocamlnum nums.cma from in /usr/bin.

Also where it says "if you are in Windows you should copy this file to pa_j.ml" that actively didn't work for me, and just running make seems to work so far.
Tags: formal systems, hol, math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 5 comments