- Minor nit: The documentation mentions "uvx aristotlelib@latest aristotle" but that doesn't work; it should be "uvx --from aristotlelib@latest aristotle"

- It took me a minute or two of clicking around to figure out that the (only?) way to use it is to create an API key, then start aristotle in the terminal and interact with it there. It could be more obvious I think.

- Your profile links to http://www.cs.stanford.edu/~tachim/ which doesn't work; should be http://cs.stanford.edu/~tachim/ (without the www) (I think Stanford broke something recently for the former not to work.)

This deserves a HN thread in its own right! Do you want to submit it and email [email protected] so we can put it in the SCP (https://news.ycombinator.com/item?id=26998308)?

Edit: I just realized from https://news.ycombinator.com/item?id=46296801 that you're the CEO! - in that case maybe you, or whoever you think most appropriate from your organization, could submit it along with a text description of what it is, and what is the easiest and/or most fun way to try it out?

Do you regularly test your AI on the https://github.com/google-deepmind/formal-conjectures collection?