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.

Today, we're releasing two big improvements to Acorn's type system. The first is typeclasses.

There's a useful new feature in Acorn Prover 0.0.8: a build cache.

When you save changes to an Acorn project, the AI model automatically completes simple proofs with missing steps. Usually this works great, but this can make refactoring more difficult. In particular, if you make changes to a module like nat.ac that many other modules depend on, it can be slow to rebuild everything. If you want to remove a theorem that is used in many places, this can involve many slow rebuilds.

We've deployed a new version of the Acorn Prover, 0.0.5, with support for a commonly requested feature: generic types. For example, the standard library now has a Pair structure:

structure Pair<T, U> {
    first: T
    second: U
}

Good news, everybody!

With this blog post, I hereby demonstrate that the Acorn blog is now capable of handling posts.