GEO00: The Geometry route: seven phases, four bridges, one visual language
On this page
- A. Prerequisites and observable goals
- B. The destination, and the route
- C. How this track teaches
- D. The visual language
- D.1 Colours and marks
- D.2 The hero diagram
- D.3 The build-up strip
- D.4 The worked-solution sequence
- D.5 The trap figure
- D.6 The toolbox card
- Toolbox card S: The inscribed angle theorem (sample)
- D.7 The interactive explorer
- D.8 How the figures are made
- E. Phase by phase, module by module
- Phase 1: Foundations (50 hours)
- Phase 2: Circles (55 hours)
- Phase 3: Trigonometry in geometry (32 hours)
- Phase 4: Coordinates and vectors (36 hours)
- Phase 5: Triangle centres and classic theorems (42 hours)
- Phase 6: Advanced circles and transformations (46 hours)
- Phase 7: Olympiad strategy (48 hours)
- F. The capstone problem
- G. Where geometry meets the Engineering Lab and competitive programming
- H. Prove it without AI: how each phase ends
- I. Hours, pace, and honest limits
- J. How every answer and figure is checked
- Sources for section C’s 2026 facts (checked 17 October 2026)
A. Prerequisites and observable goals#
Nothing. Read this chapter first, then take GEO01’s diagnostic.
Describe the seven phases and 28 modules, their hours, and the four bridge modules that link geometry to CAD and to competitive programming; say where each module meets the Engineering Lab and the algorithms lane; read every figure in this part using the visual language, and know how each kind of figure is built and checked; state the capstone problem and where it is solved; know how each phase ends without AI; know how every answer and figure in this part is verified.
Level: Track plan. This book teaches the track’s first module, GEO01, in full; this chapter is the map of the whole route: what each later module covers, how long it takes, and what it leads to. The hours are estimates; log your real hours and re-plan the rest from them.
B. The destination, and the route#
By the end of this track you will be able to solve geometry problems the way strong competitors do: chase angles and ratios through a figure, choose between a synthetic argument and a computation, prove what you claim in a write-up a grader accepts, and handle the circle configurations (tangent circles, power of a point, radical axes, homothety, inversion) that make up much of olympiad geometry. Along the way, geometry becomes two practical tools: the constraint language of every CAD sketch you will draw in the Engineering Lab, and a family of exact algorithms (orientation tests, intersections, convex hulls) that competitive programming and robotics code rely on.
The route: seven phases (the stations), each ending with a closed-book test, and four bridge modules (blue) that branch off where their prerequisites are met and where the Engineering Lab or the algorithms lane needs them. The capstone problem closes Phase 2 and returns in Phase 6.
C. How this track teaches#
Every module follows the same shape, so you always know where you are.
- A diagnostic first (GEO01 only), and from GEO02 on, a spaced review of two or three questions drawn from your error log: one row per miss, with the problem, the mistake’s name, the first wrong step, the corrected rule, and the date to review it next.
- A quick summary that opens with a picture of the real mechanism, five core ideas, and a session plan.
- A deep explanation. Every theorem is derived before it is used, with one small example worked with complete algebra, every symbol defined, and a hero diagram plus a build-up strip that draws the proof one move at a time. Faded examples, “say it back” prompts, and named misconceptions sit inside the explanation, not after it.
- Guess, then prove. Before every problem with a figure, you estimate the answer from the figure, which is drawn exactly unless it says otherwise. Then you prove it and see how close you were. Your guesses sharpen, and a big miss is a signal to recheck.
- Several approaches. Worked examples are solved at least two ways and the ways are compared, because choosing a method is the skill olympiads test hardest.
- Named mistakes. Each module has a field guide of the mistakes beginners make (trusting the diagram, assuming a midpoint, mixing up inscribed and central angles, circular reasoning, and so on), with the symptom and the check that catches each one. Your error log counts them by name.
- Practice in three tiers: drill (one move until it is automatic), problems (several moves or a written proof), and challenges (an idea you have to find). Every problem has a three-rung hint ladder (a question, a pointer to the idea, a skeleton with blanks), and every solution, with its own figure sequence, sits in a separate section that you open only after an attempt.
- Toolbox cards: one page per theorem, with one diagram, the statement, when to reach for it, and the trap to avoid. Review them like flashcards at 2, 7, and 21 days.
- Does it say what was meant? From GEO02 on, each problem set includes a restated problem to check against the original, sometimes faithful and sometimes subtly changed (a dropped condition, a point on the wrong arc, “inside” turned into “on”), and you decide which before solving. In 2026 this became a scarce skill: a system that translated olympiad geometry problems into a proof language for machines got the statement wrong for 14 of 43 of them, and mathematicians now argue that no machine proof should be accepted until a human has audited its statement.
- Proofs graded like an olympiad. Written proofs are graded on the 0–7 scale olympiads use, by a teacher, a study partner, or you against the complete solutions. In a repair round the grader names only the defect, never the fix, and you rewrite the proof yourself.
- A mastery gate: a closed-book quiz, a teach-back, the cards from memory, and your guess record. You move on only when it passes.
- A development-log entry, and optional stretch work, clearly marked, where advanced insight lives. Nothing advanced is dropped; it is sequenced. Machine-checked proof in the Lean proof assistant is one such stretch, not a requirement, because the evidence that it helps beginners learn proof is mixed.
- Everything is in this book. The track sends you to no outside books or websites; the only site it uses is the book’s own companion website, for the interactive explorers. Its problems are original, and its explanations are written for you.
- AI in three zones, as Part I’s chapter on learning (LM) sets them: none on first attempts, guesses, proofs, or gates; concepts and hints only after a logged attempt, each use noted in an AI-use log (the date, the task, what you asked, and what you then did yourself); chores any time.
D. The visual language#
Diagrams are the spine of this track, so every figure follows one set of rules. The legend on the first page of this part is the short version; this section is the full one, with one sample of every kind of figure. The samples use circle geometry from Phase 2 on purpose: they show that tangent points, right angles, and midpoints come out exact, which is the hardest thing for a figure to get right.
D.1 Colours and marks#
| Role | Colour | Second cue (never colour alone) | Meaning |
|---|---|---|---|
| Given | black | solid lines | stated in the problem |
| Auxiliary or constructed | blue (EL blue) | dashed lines | drawn by the solver |
| Target | red (EL red) | a question mark | what you must find or prove |
| Proved | green (EL aqua) | a check mark | established in this solution |
| New in this frame | yellow band | a highlighter stroke underneath | the one move this frame adds |
Equal segments carry the same number of tick marks, equal angles the same number of arcs, parallel lines the same number of arrows, and right angles a small square. A mark appears only when the problem states the fact or a proof has established it, never because it looks true.
The blue, red, and green are the Engineering Lab’s validated palette, reused so the two tracks look like one book. Simulated for the three kinds of dichromatic colour vision, every pair stays apart, but two pairs come closest: red and green for deuteranopia, a common red–green deficiency (a CIEDE2000 colour difference of about 13), and blue and green for tritanopia, a rare blue–yellow one (about 15). Every other pair differs by 16 or more. Thin lines make small differences harder to see, which is why no colour works alone: a target always carries its question mark and a proved fact its check mark.
D.2 The hero diagram#
Every theorem gets one hero diagram: the single picture that shows why it is true, drawn exactly, labelled lightly, and reused on its toolbox card.
D.3 The build-up strip#
Every theorem also gets a build-up strip: its proof drawn one move per frame, each new mark on a yellow band, and a one-line caption that names the reason. Read a strip left to right, top to bottom; cover the captions and say each reason yourself.
D.4 The worked-solution sequence#
Every worked solution gets its own sequence of frames instead of one crowded diagram. The problem view comes first; the solution frames follow the written steps one to one.
D.5 The trap figure#
Trap figures train your suspicion. Some are exact and still mislead the eye; others are marked not to scale, as contest figures sometimes are.
D.6 The toolbox card#
Each theorem’s card fills one page, so it can be printed or flipped through as a flashcard. The next page is a sample card for a theorem from Phase 2.
Statement
An inscribed angle is half the central angle that stands on the same arc: . Consequences: inscribed angles on the same arc are equal, and an angle inscribed in a semicircle is a right angle.
Reach for it when
A circle has a chord and a point on the circle; you need an angle at the circle from one at the centre, or the reverse; two angles stand on the same arc.
Watch out
The centre may lie outside the inscribed angle: the theorem still holds, but the proof subtracts instead of adding. And an inscribed angle is not the central angle: halve it (mistake: mixing up inscribed and central angles).
Review this card at 2, 7, and 21 days: cover everything but the title, say the statement and draw the diagram, then check.
D.7 The interactive explorer#
For the key invariants, a figure you can move beats any static one. Each explorer is a self-contained web page on the companion website, linked from its module: you drag points and watch measurements change while the invariant stays fixed. A saved copy of the page works offline.
- GEO01, the Angle Explorer (
bezhig.com/book/explorers/geo01-angles.html): triangle angle sums, parallel lines and a transversal, the bent arrow, and the five-pointed star. It is this style guide’s sample explorer. - Planned on the route, with their modules: the inscribed angle (GEO06), power of a point (GEO09), the radical axis (GEO21), and the homothety of tangent circles (GEO22).
D.8 How the figures are made#
This part’s figures are drawn in TikZ with the tkz-euclide package and a small shared style library. Five rules make them trustworthy.
- Construct, never eyeball. Points come from constructions from the givens: intersections, perpendicular bisectors, tangents from a point, rotations. A coordinate typed by hand is allowed only for a free choice, such as the length of a base.
- Every figure asserts its measures. While a figure compiles, it measures its own angles, lengths, tangencies, and midpoints and records them; the build fails if any misses the value the problem states. Asserting in an unscaled view keeps TeX’s arithmetic precise to about cm.
- One scene, many frames. A figure defines its geometry once, and each mark declares the frame in which it appears. The problem view, every frame of a strip, and the hero are views of the same construction, so they cannot disagree.
- Drawn at final size. Figures are printed at the size they were drawn, so labels match the text and lines are the same weight everywhere. The few drawn wider than this book’s text block are reduced to fit, by about 5% at most.
- Looked at before you see them. Every figure is rendered and inspected for overlapping labels, clipping, and marks that do not match the text.
E. Phase by phase, module by module#
This book teaches GEO01 in full; the other entries are the route’s map. Hours include practice, the gate, and the development log. “Meets” names the Engineering Lab (EL) modules and the algorithms lane that each module feeds; those tracks, too, teach their first module in this book and map the rest. Bridge modules are marked B.
Phase 1: Foundations (50 hours)#
- GEO01 Angle chasing and your first proofs (in this book; 10 h). The diagnostic; angles and parallel lines; the triangle angle sum and the exterior angle theorem from the parallel postulate; isosceles triangles; polygon angle sums; how to write a proof, and the traps of diagrams. Meets: the algorithms lane through its stretch (the orientation test in C++).
- GEO02 Congruence (10 h). SAS as the starting postulate; ASA, SSS, AAS, and the right-angle rule proved from it; why SSA fails, drawn exactly; perpendicular bisectors and angle bisectors as sets of points; compass-and-straightedge constructions. Meets: EL01’s parametric part and EL11’s sketches (three lengths fix a triangle, so three dimensions fully constrain it), and the rigidity of triangulated frames (EL07, EL12).
- GEO03 Similarity and ratio chasing (10 h). AA, SAS, and SSS similarity; the intercept theorem; the angle bisector theorem; ratio chasing; scale drawings. Meets: drawings at scale (EL10), and the similar triangles hidden in related-rates problems (Module 12).
- GEO04 The Pythagorean theorem (8 h). Four proofs (dissection, similar triangles, area, a trapezoid); the converse; the 30–60–90 and 45–45–90 triangles; the distance formula. Meets: force components (EL01.13, EL02), which the Engineering Lab teaches; this module supplies the geometry, not a second copy of the physics.
- GEO05 Area methods (8 h). Area from base and height; equal-base and equal-height ratios; area proofs; a first look at the shoelace formula. Meets: polygon area in code (B4) and section areas (EL07).
- Phase 1 test (4 h).
B1: 3D geometry for CAD, part 1: solids, sections, and projections (8 h, after Phase 1). Points, lines, and planes in space; prisms, pyramids, cylinders, cones, and spheres; cross-sections; orthographic front, top, and side views, and first- versus third-angle projection; isometric views; hidden lines; volumes by slicing (Module 18). Meets: EL10’s drawings and EL11’s views, and the hidden-line drawings that the Engineering Lab’s hardware engine makes from EL01 on.
Phase 2: Circles (55 hours)#
- GEO06 Inscribed and central angles (10 h). Chords and arcs; the inscribed angle theorem in all three cases; Thales’ theorem; equal chords and equal arcs. Explorer: the inscribed angle.
- GEO07 Tangents (9 h). A radius is perpendicular to its tangent; equal tangents from a point; the tangent–chord angle; the incircle and its tangent lengths; tangent constructions. Meets: tangent arcs and fillets in sketches (B2).
B2: CAD sketches as geometry (8 h, after GEO07). The constraint vocabulary (coincident, tangent, concentric, perpendicular, parallel, horizontal and vertical, equal, symmetric, and dimensions), each as the geometry fact it enforces; degrees of freedom (a point has 2, a line 2, a circle 3) and how constraints remove them; fully constrained, under-constrained, and over-constrained sketches, and redundant versus conflicting constraints; construction geometry; the capstone configuration built as a fully constrained sketch in build123d, and the same sketch’s constraints named in Siemens NX. Meets: EL01 (build123d), EL11 (sketches and constraints in NX), and EL12 (the frame).
- GEO08 Cyclic quadrilaterals (10 h). Opposite angles supplementary, and the converse; equal angles on the same chord as a test for four points on a circle; cyclic quadrilaterals in angle chasing; Ptolemy’s theorem (stretch).
- GEO09 Power of a point (10 h). Intersecting chords, two secants, a tangent and a secant; power as ; a first look at the radical axis. Explorer: power of a point.
- GEO10 Common tangents, tangent circles, and the capstone (12 h). Lengths of common external and internal tangents; tangent circles; the capstone solved three ways: power of a point with the tangent–chord angle, right-triangle trigonometry, and coordinates.
- Phase 2 test (4 h).
Phase 3: Trigonometry in geometry (32 hours)#
- GEO11 The law of sines (10 h). Sine and cosine as projections, seen from the geometric side (Module 04 has the unit circle; EL02 resolves forces with it); the law of sines; the extended law from the inscribed angle; the ambiguous case, which is GEO02’s failure of SSA in numbers.
- GEO12 The law of cosines and area formulas (10 h). The law of cosines from Pythagoras; , Heron’s formula, , and ; solving any triangle.
- GEO13 Trigonometry as a problem-solving tool (8 h). When to compute with trigonometry and when not; the ratio lemma; a first look at trigonometric Ceva.
- Phase 3 test (4 h).
Phase 4: Coordinates and vectors (36 hours)#
- GEO14 Analytic geometry: choosing coordinates (10 h). Lines, circles, and the distance from a point to a line; choosing axes that keep the algebra small; coordinate proofs.
- GEO15 Vectors: the dot and cross products from the geometric side (10 h). The dot product as projection and as the test for perpendicular lines; the 2D cross product as signed area and as orientation; vector proofs. EL02 teaches vectors and torque first; this module adds only the geometry, and points back to it.
B3: 3D geometry for CAD, part 2: planes, normals, and rotations (10 h, after GEO15). Lines and planes in vector form; distances and angles between lines and planes; the 3D cross product; rotations about an axis as geometry (two reflections make a rotation); rotation matrices from the geometric side. Meets: EL18 (rotations and frames), which starts just before it when you take both tracks together, EL12’s clearances, and EL19’s inertia from CAD.
B4: Computational geometry in C++ (14 h, after B3). Exact predicates with integer arithmetic; orientation; segment intersection; polygon area; point in polygon; the convex hull by monotone chain; circle–line and circle–circle intersections; tangents from a point and common tangents; floating-point robustness; original contest-style problems with tests you run. Meets: the algorithms lane (C07–C08, and F17 on F00’s map). If the lane needs geometry sooner, B4’s first half (orientation, intersection, area, hull) can run right after GEO05, using EL02’s cross product.
- GEO16 Complex numbers as a geometry tool (12 h). Points as complex numbers; rotation as multiplication; the unit-circle setup; tests for collinear, perpendicular, and concyclic points; when complex numbers win.
- Phase 4 test (4 h).
Phase 5: Triangle centres and classic theorems (42 hours)#
- GEO17 The four classic centres (10 h). Centroid, circumcentre, incentre and excentres, orthocentre; why each set of three lines meets at one point; the incentre–excentre lemma. Meets: the centroid is a uniform triangle’s centre of mass (EL02).
- GEO18 Ceva and Menelaus (10 h). Both theorems and their converses; trigonometric Ceva; concurrence and collinearity; mass points (stretch).
- GEO19 Stewart’s theorem and lengths in triangles (8 h). Stewart’s theorem; median and bisector lengths; when computing beats a synthetic argument.
- GEO20 The Euler line and the nine-point circle (10 h). The Euler line; the nine-point circle; reflections of the orthocentre; the Simson line.
- Phase 5 test (4 h).
Phase 6: Advanced circles and transformations (46 hours)#
- GEO21 Radical axis and radical centre (10 h). The radical axis of two circles; the radical centre of three; families of circles sharing an axis. Explorer: the radical axis.
- GEO22 Homothety and tangent circles (10 h). Homothety; the two centres of similitude; tangent circles; Monge’s theorem; the capstone revisited by homothety. Explorer: the homothety of tangent circles.
- GEO23 Inversion (12 h). What inversion does to lines and circles; inverting tangent circles; Pappus and Steiner chains (stretch); the capstone revisited by inversion.
- GEO24 Spiral similarity and the Miquel point (10 h). Centres of spiral similarity; Miquel’s theorem; the complete quadrilateral.
- Phase 6 test (4 h).
Phase 7: Olympiad strategy (48 hours)#
- GEO25 Choosing a method (12 h). Synthetic, complex numbers, coordinates, trigonometry, and a first look at barycentric coordinates; how to decide in the first five minutes; timed practice.
- GEO26 Projective basics (14 h). Cross-ratio; harmonic divisions; poles and polars; the theorems of Pascal, Brianchon, and Desargues.
- GEO27 Writing olympiad proofs (10 h). Configuration issues and how to handle them; how a seven-point grading scale treats gaps; regrading your own old solutions.
- GEO28 Mock olympiad and the final closed-book test (12 h).
| Phase | Modules | Hours | Running total |
|---|---|---|---|
| 1. Foundations | GEO01–GEO05, test | 50 | 50 |
| B1 | 3D for CAD, part 1 | 8 | 58 |
| 2. Circles, with B2 | GEO06–GEO10, test; B2 after GEO07 | 55 + 8 | 121 |
| 3. Trigonometry | GEO11–GEO13, test | 32 | 153 |
| 4. Coordinates and vectors, with B3 and B4 | GEO14–GEO16, test; B3 and B4 after GEO15 | 36 + 24 | 213 |
| 5. Triangle centres | GEO17–GEO20, test | 42 | 255 |
| 6. Advanced circles | GEO21–GEO24, test | 46 | 301 |
| 7. Olympiad strategy | GEO25–GEO28 | 48 | 349 |
| Total: 28 modules, 4 bridges, 6 phase tests and a final | 349 | ||
F. The capstone problem#
On the route, GEO10 solves it with power of a point and the tangent–chord angle, with right-triangle trigonometry, and with coordinates. GEO22 solves it again with a homothety, and GEO23 with an inversion. Comparing five solutions of one problem is the best lesson this track has in choosing a method. Those modules lie beyond this book, so here the capstone stays open: keep your guess, and test it when your tools reach it.
G. Where geometry meets the Engineering Lab and competitive programming#
| Where | What it needs | Where this track provides it |
|---|---|---|
| EL01, first part in build123d | A shape fixed by its dimensions | GEO02 (congruence as rigidity); B2 |
| EL01.13, tilted thrust | Right-triangle trigonometry | GEO04, GEO11 |
| EL02, vectors, moments, centre of mass | Components, the 2D cross product, centroids | GEO15, GEO17, GEO05 (EL02 teaches the physics first) |
| EL07, beam sections | Areas of cross-sections | GEO05, B1 |
| EL10, drawings and GD&T | Orthographic views, scale, datums as geometry | B1, GEO03 |
| EL11, sketches and constraints | The constraint vocabulary, degrees of freedom | B2, GEO07, GEO02 |
| EL12, frame and clearances | Distances between lines and planes | B3 |
| EL18, rotations and frames | Rotations as geometry | B3, GEO16 |
| EL19, inertia from CAD | Planes, normals, and solids | B1, B3 |
| Algorithms lane, C07–C08, F17 | Orientation, intersections, hulls, exact arithmetic | B4 (early start possible after GEO05) |
| Calculus, Modules 12 and 18 | Similar triangles in related rates; volumes by slicing | GEO03, B1 |
The Engineering Lab teaches vectors (EL02) and rotations (EL18) for forces and frames; this track teaches their geometry and points back rather than repeating them.
H. Prove it without AI: how each phase ends#
Every phase ends with a closed-book test on paper, with no notes and no AI: original problems in the phase’s style, and one proof you write out in full. Mark it against its rubric, or have a teacher or study partner mark it: name the first incorrect step of each miss, and log every gap in your error log. The gaps become the next phase’s spaced review.
| Phase | The test (about 2 hours of the 4) | The written proof |
|---|---|---|
| 1 | Five problems: an angle chase with parallels, an isosceles chain, a similar-triangle ratio, a Pythagorean length, an area ratio | A congruence proof, two-column |
| 2 | Five problems on inscribed angles, tangents, cyclic quadrilaterals, and power of a point, one of them the capstone’s style | A cyclic-quadrilateral proof, as a paragraph |
| 3 | Four problems solved by the laws of sines and cosines and the area formulas | The extended law of sines, from scratch |
| 4 | Four problems: one each by coordinates, vectors, and complex numbers, and one of your choice; plus a C++ predicate written on paper | A vector proof |
| 5 | Four problems on centres, Ceva, Menelaus, and Stewart | The nine-point circle, or Ceva’s theorem |
| 6 | Four problems on radical axes, homothety, and inversion, one of them the capstone again | A radical-centre or homothety proof |
| 7 | A mock olympiad: three problems in three hours, graded on a seven-point scale | All three, in full |
I. Hours, pace, and honest limits#
The track is about 349 hours. At 4 hours a week that is about 87 weeks, roughly 20 months; at 6 hours a week, about 13 months; at 3 hours, about 27. If you take the Engineering Lab beside it, at about 9 hours a week with both tracks started together, each bridge comes before the Engineering Lab module that needs it: B1 (projections) is done after about 15 weeks, well before EL10’s drawings begin at about 22; B2 (sketches) is done after about 21 weeks, before EL11’s sketches begin at about 24; and B3 (rotations) starts at about 43 weeks, just after EL18 begins, and adds its geometry.
The Geometry route at 4 hours a week, in months from the start, with the three Engineering Lab modules the bridges serve, placed from EL00’s route at 9 hours a week with both tracks started together. “Plan your path” in Part I shows how to fit this track beside a course and the other tracks. A plan, not a promise: your real hours re-plan it.
Honest limits.
- Time competes. Four hours a week of geometry is a real share of a week that may also hold a course, the Engineering Lab, or the AI Lab. The diagnostic can shorten Phase 1; if the plan slips, protect the bridges before the olympiad phases, because the bridges feed the other tracks.
- What 349 hours buys. Fluency with the geometry of national olympiads at moderate difficulty, proofs that graders accept, and the CAD and computational-geometry skills of the bridges. The hardest olympiad geometry takes several hundred more hours of problem solving. Phase 7 ends by setting you up to continue on your own.
- Interviews. Engineering and AI interviews weigh algorithms and systems more than geometry. B4 turns geometry into algorithm practice, which is why it can start early.
J. How every answer and figure is checked#
Nothing in this part reaches you unchecked.
- Every numeric answer was recomputed by script with a coordinate model that builds each configuration from its givens, not from the solution’s chase, and compared with the stated answer.
- Every figure is constructed from exact geometry and asserts its own measures while it is built (section D.8); a figure that misses a stated value does not build. Every problem has exactly one solution, and every practice problem exactly one hint ladder; both are checked mechanically.
- Every problem was also worked cold, from its statement alone and before its solution was read, to confirm that it is solvable with the module’s tools, unambiguous, and has the stated answer.
- Every proof was checked for gaps and circular steps, every explanation for accuracy, and every figure against its caption and for overlapping labels, clipping, clutter, and marks that do not match the text.
Sources for section C’s 2026 facts (checked 17 October 2026)#
These verify facts and are not study material. MechGeo, machine-checked proofs of olympiad geometry and its 14 wrong statements out of 43 (August 2026), arxiv.org/abs/2608.02295; Thomas Hales on auditing the statements of machine proofs, on Terence Tao’s blog (9 October 2026), terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/; Hanna, Larvor and Yan on using Lean in undergraduate classrooms (mixed evidence for beginners), www.researchgate.net/publication/379996027_Using_the_proof_assistant_Lean_in_undergraduate_mathematics_classrooms.