Getting More out of Large Language Models for Proofs

Code that ran

We have not lifted any functions out of this paper's repositories yet, so there is nothing we have run. If it links a repository, it is listed below.

Abstract

Large language models have the potential to simplify formal theorem proving and make it more accessible. But how to get the most out of these models is still an open question. To answer this question, we take a step back and explore the failure cases of these models using common prompting-based techniques. Our talk will discuss these failure cases and what they can teach us about how to get more out of these models.

For agents

The same record, over MCP at https://syntology.ai/mcp:

get_harvested_code_for_paper("2305.04369")
get_code_for_paper("2305.04369")
have("2305.04369")

Connect an agent — have() is free.