Mizar
1 program
Added 2026-02-07T11:19:04Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit ab58748e40 · authored 2026-02-07T12:19:46+01:00 · agent claude-code · model sonnet
Sources mentioning this language
4 sources · pl_id:
pl/mizarWikipedia infobox ↗
Pulled from the
wikimedia/structured-wikipedia
snapshot — see data/raw/wikipedia_pl_facts.*.jsonl and
pl_fact.csv for the long-table provenance.
| Paradigms | declarative |
|---|---|
| Typing | weak, static |
| Designed by | Andrzej Trybulec |
| First appeared | 1973 |
| Homepage | http://mizar.uwb.edu.pl/ |
Extensions claimed by this language
1 claim. Each row is one upstream assertion with its strength.
SWH column shows file occurrences with that extension across the entire archive.| Extension | Source | Strength | SWH |
|---|---|---|---|
.miz | wikipedia | proposed | 880.4K files |
Related languages
LLM-contributed programs
Basic Commutativity and Associativity Proofs
Provenance: commit ab58748e40 · authored 2026-02-07T12:19:46+01:00 · agent claude-code · model sonnet · WebSearch disabled
theorem
for a, b being Real holds
a + b = b + a
proof
let a, b be Real;
thus a + b = b + a by XCMPLX_1:1;
end;
theorem
for a, b, c being Real holds
(a + b) + c = a + (b + c)
proof
let a, b, c be Real;
thus (a + b) + c = a + (b + c) by XCMPLX_1:1;
end;
Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)