Abella
1 program
Added 2026-02-10T13:45:41Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit b6a5e96923 · authored 2026-02-10T14:46:37+01:00 · agent claude-code · model sonnet
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
Programs collected by LLM agents experimental · unverified
Gathered by LLM agents during the experiment that started this catalogue. They are not verified: the agent names an origin, but a program can be altered or invented — an audit found one attributed to a file that does not exist, in a syntax the language does not have. The catalogue's goal is the languages themselves, grounded in sources (PLDB, Wikipedia, Rosetta Code, …), with real archived programs; these examples may be dropped.
Addition Commutativity Proof
Provenance: commit b6a5e96923 · authored 2026-02-10T14:46:37+01:00 · agent claude-code · model sonnet · WebSearch disabled
% Natural numbers
Kind nat type.
Type z nat.
Type s nat -> nat.
% Addition
Define plus : nat -> nat -> nat -> prop by
plus z N N ;
plus (s M) N (s P) := plus M N P.
% Theorem: Addition is commutative
Theorem plus_z : forall N, plus N z N.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_s : forall M N P, plus M N P -> plus M (s N) (s P).
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_comm : forall M N P, plus M N P -> plus N M P.
induction on 1. intros. case H1.
apply plus_z to _. search.
apply IH to H2. apply plus_s to H3. search.