Gergely Buday (Mar 02 2026 at 10:55): Gergely Buday (Mar 02 2026 at 10:55):Hi there,
which popular web-based generative artificial intelligence knows the Archive of Formal Proofs deeply? I would like to ask questions on where some constructs are used, and so on.
Or, is there an open source alternative that I could host locally and train on the latest AFP version?
Maximilian Schäffeler (Mar 02 2026 at 11:20):Hi,
in my experience, most Chatbots are likely to hallucinate contents of AFP entries. To get a rough overview, Gemini 3 in thinking mode worked ok in my testing. I did not try out using Claude Code/etc. to feed in the AFP locally.
If you actually intend to use the AFP entry yourself, I would guess that currently you will still be faster and gain more understanding using search tools such as FindFacts and SErAPIS.
Last updated: Mar 20 2026 at 05:16 UTC