The Acorn Theorem Prover Blog
Freek Wiedijk's list of one hundred mathematical theorems has long served as a compact way to understand the reach of a theorem-proving system. It is broad enough to touch much of ordinary mathematics, but concrete enough that progress can be measured theorem by theorem. A prover that makes progress on the list has to do more than manipulate syntax. It needs a library, a mathematical vocabulary,…
Constrained types in Acorn now have a simple, explicit constructor behavior: new returns an Option.
We're making a big change to the Acorn syntax: using square brackets for type parameters, instead of angle brackets.
Acorn 0.1 is out! It might not be obvious at first, but there's a big change in the guts of how the prover works. When a proof is successfully verified, the build directory now contains a "proof certificate" explaining step by step how the proof works.
Typeclasses in Acorn provide a powerful way to define common behaviors across different types. But what happens when you need to build upon existing typeclasses? Today, we're introducing typeclass extension.
Since launching the Acorn beta, we've heard consistent feedback from mathematicians that they need a powerful type system to represent their favorite area of mathematics.
There's a useful new feature in Acorn Prover 0.0.8: a build cache.
We've deployed a new version of the Acorn Prover, 0.0.5, with support for a commonly requested feature
Good news, everybody!