Jason (jcreed) wrote,

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

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded