> ... But in some cases, Aristotle can define the structure you are talking abou... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

zozbot234 6 months ago | parent | context | favorite | on: “Erdos problem #728 was solved more or less autono...

> ... But in some cases, Aristotle can define the structure you are talking about on the fly! ...

Do you have any plans to characterize these cases more fully, and perhaps propose your own contributions to mathlib itself on that basis?

tachim 6 months ago [–]

There have been many contributions to mathlib from Aristotle already, it’s a major use case for our users

Consider applying for YC's Fall 2026 batch! Applications are open till July 27.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact