Qualifying exam solutions¶
Forty-three qualifying examination papers from the graduate mathematics program at the University of Hawaii at Manoa, set between 1991 and 2008 in group theory, ring theory, real analysis and complex analysis, with worked solutions I wrote over several years. The solutions were written as a single document rather than as forty-three answer keys, and that is what made it slow: they carry 81 cross-references and an index of 42 subject headings, so each one has to agree in notation and in approach with every other solution touching the same material, and a problem that reappears in a later year under different words has to be recognized as the same problem and answered once. The corpus is served at formalverification.io/exams/, and the section below says exactly how much of the solution text has reached the web and how much is still sitting in the page source.
Sole author · 2009– · maintained
real analysis complex analysis algebra
The problems are the department's; the solutions are mine¶
The problems were set by the mathematics faculty at Manoa and are reproduced as they were given. The worked solutions are my own, and they are the only original content here. Where a solution follows a standard argument it is the standard argument; where it does not, the approach is mine and is not necessarily the one the examiners had in mind.
What is published, and what is still in the source¶
| Subject | Papers |
|---|---|
| Ring theory | 13 |
| Complex analysis | 12 |
| Group theory | 11 |
| Real analysis | 7 |
| Total | 43 |
All 43 papers are published. Worked solutions are visible on four of them: November 2008 in ring theory, April 1998 and November 1994 in real analysis, and November 2000 in group theory.
A further 48 worked solutions are written but not yet published. They sit
in the page source as commented-out LaTeX, on twelve more papers, and they are
the reason the next piece of work is conversion rather than authoring. This is
checkable without taking my word for it: view the source of
April 1995 in complex
analysis and six of them are there, in \begin{solution} environments, with the
index entries and cross-references intact.
The collection is incomplete by design and expected to grow. Its own cross-references name four sittings that have not been digitized at all: April 1989, April 1992, November 1996 and November 1997.
Formalization in Agda: planned, not begun¶
The intent is to formalize solutions in Agda beside the prose, one exam at a time, so a page carries both the argument a reader follows and the proof a typechecker accepts. The algebra half sits naturally next to agda-algebras, which already formalizes the group and ring theory these problems assume, and it supplies something that library does not otherwise have: a large body of mathematics that nobody wrote with it in mind. That is what makes it a test rather than a demonstration, and it is the reason the corpus was given its own public repository instead of being served from this site.
None of this exists yet. The corpus repository contains zero .agda and
zero .lagda files. This page will keep saying so until that changes.
The two analysis collections¶
Earlier presentations of the same problems are still online as separate Sphinx sites, Exercises in Real Variables and Exercises in a Complex Variable. They were advertised as two further book projects on the previous version of this site; they are not. They are the real and complex halves of this corpus in an earlier form, and ADR-002 folded them in here rather than listing them again, because one body of work should not be advertised twice. They are linked above as artifacts, not as projects.
Artifacts¶
- The corpus: all 43 papers in four subjects, with per-subject indexes and a year-by-year table. This is the thing itself.
- Source: public,
and the place to check the claim about the 48 unpublished solutions, which
are in
docs/exams/in plain sight. - Exercises in Real Variables and Exercises in a Complex Variable: the earlier Sphinx presentations of the analysis half.
- agda-algebras: the library the algebra formalization will be built on, and the reason the corpus is worth formalizing rather than merely finishing.
What is next¶
- Convert the 48 solutions already written. Mechanical, and it roughly trebles the published solution text.
- Digitize the four missing sittings the existing solutions already cite.
- Formalize one solution end to end, in algebra, against
agda-algebras. One is the number that matters: until a solution goes from prose to machine-checked proof, the formalization is an intention, and a page that describes an intention as work is worth less than no page.
Every URL the older versions of this site served for these pages still resolves.