Meta tags:
description=Mathematicians learning Lean by doing.;

Headings (most frequently used words):

the, ai, is, what, of, in, mathematics, do, it, formalization, theorem, are, how, approach, with, formal, think, number, lean, let, uses, growing, problem, human, worries, about, to, this, language, models, questions, quotient, can, frontiermath, fermat, last, 2024, xena, accelerating, traditional, duh, just, llms, itps, itp, libraries, humans, computers, tl, dr, erdős, problems, background, without, entirely, by, side, notes, misformalization, takeaways, acknowledgments, or, not, that, question, for, proving, non, informal, whose, job, fix, at, imo, 2025, round, up, setting, scene, deciding, rules, results, summary, an, update, and, answering, wrong, current, status, experiment, lessons, learnt, natural, numbers, well, defined, functions, universal, property, done, appendix, quotients, made, we, test, make, database, will, look, like, maths, yet, thoughts, from, mathematician, o3, hard, dataset, exactly, has, happened, here, prove, who, marking, machines, going, modern, focused, research, organisation, user, base, computer, science, else, come, categories, recent, posts,

Text of the page (most frequently used words):
the (1085), and (469), that (301), this (270), are (197), which (188), mathematics (160), for (154), lean (149), have (143), not (139), was (135), but (129), with (118), they (106), you (102), what (102), can (98), from (88), will (86), problems (82), #questions (78), were (76), problem (75), one (73), about (71), there (71), more (66), then (65), these (61), all (61), #language (59), would (59), proof (59), now (58), theorem (57), even (57), had (55), just (51), because (50), number (49), how (49), been (49), has (48), level (47), formal (46), imo (45), some (45), also (44), like (43), question (42), research (42), when (42), many (42), such (40), here (40), get (39), other (39), who (39), human (39), them (39), very (38), right (38), models (38), theory (37), out (37), paper (37), way (36), llm (36), need (36), answer (36), being (35), model (35), post (35), 2025 (34), people (34), time (34), example (34), their (33), make (33), into (33), let (32), work (32), first (32), solution (32), only (32), using (31), see (31), mathematicians (30), solutions (30), than (30), aristotle (30), formalization (28), two (28), computer (28), results (28), undergraduate (28), actually (28), code (28), still (28), dataset (28), want (27), llms (27), well (27), numbers (27), far (26), think (25), where (25), mathematical (25), proofs (25), could (25), know (25), set (25), tech (25), posted (24), community (24), might (24), humans (24), erdős (23), 2024 (23), used (23), made (23), approach (23), library (23), solved (23), definitions (23), however (23), solve (23), last (22), new (22), seen (22), both (22), over (22), several (22), write (21), really (21), integers (21), long (21), modern (21), gold (21), chatgpt (21), already (20), mathlib (20), course (20), project (20), any (20), doing (20), use (20), above (20), going (20), things (20), got (20), don (20), prove (20), mod (20), thing (19), currently (19), seems (19), natural (19), tools (19), back (19), perhaps (19), point (19), before (19), answers (19), machine (18), our (18), year (18), able (18), give (18), done (18), completely (18), ideas (18), better (18), find (18), hard (18), given (18), function (18), companies (18), informal (18), look (17), result (17), database (17), most (17), correct (17), indeed (17), conjectures (17), although (17), after (17), quotient (17), comments (16), type (16), olympiad (16), math (16), clear (16), much (16), whether (16), systems (16), story (16), com (15), blog (15), getting (15), through (15), his (15), down (15), yet (15), part (15), progress (15), system (15), say (15), something (15), formalized (15), extremely (15), open (15), defined (15), formalisation (14), another (14), its (14), start (14), off (14), claim (14), argument (14), those (14), did (14), good (14), proving (13), fermat (13), mathematician (13), come (13), asked (13), until (13), tao (13), take (13), means (13), next (13), should (13), statement (13), frontiermath (13), deepmind (13), probably (13), available (13), your (13), quotients (13), sets (13), technical (12), full (12), working (12), groups (12), definition (12), data (12), fact (12), knows (12), group (12), prover (12), why (12), written (12), rather (12), attempt (12), least (12), understand (12), help (12), form (12), public (12), medal (12), same (12), openai (12), may (12), axiom (12), equivalence (12), typically (12), learning (11), try (11), high (11), statements (11), tool (11), different (11), interesting (11), mentioned (11), generated (11), making (11), theorems (11), cannot (11), does (11), big (11), though (11), understanding (11), machines (11), details (11), sense (11), sure (11), current (11), lot (11), certainly (11), epoch (11), company (11), define (11), useful (11), found (11), process (11), erdosproblems (11), recent (10), tagged (10), ask (10), page (10), fro (10), algebra (10), area (10), between (10), someone (10), years (10), particular (10), real (10), xenaproject (10), cohomology (10), job (10), since (10), wrong (10), expert (10), check (10), output (10), alphaproof (10), each (10), note (10), element (10), quot (10), odd (10), formalize (10), general (9), rules (9), science (9), researchers (9), langlands (9), basic (9), non (9), ways (9), own (9), students (9), away (9), original (9), writing (9), few (9), around (9), divided (9), issue (9), thus (9), standard (9), instead (9), case (9), trying (9), quite (9), either (9), state (9), bit (9), doesn (9), again (9), percent (9), field (9), within (9), clearly (9), taught (9), recently (9), simple (9), difficult (9), counterexample (9), developments (9), mean (9), resolved (9), itp (9), artificial (8), intelligence (8), always (8), anyone (8), kind (8), huge (8), undergraduates (8), together (8), july (8), examples (8), five (8), teaching (8), conjecture (8), enough (8), earlier (8), ago (8), certain (8), crystalline (8), experts (8), correctly (8), told (8), antoine (8), papers (8), old (8), happens (8), computers (8), idea (8), phd (8), read (8), hundreds (8), provers (8), techniques (8), exams (8), exam (8), beyond (8), large (8), 100 (8), simply (8), itself (8), axioms (8), homomorphism (8), traditional (8), believe (8), relevant (8), autonomously (8), mark (8), xena (7), maths (7), imperial (7), geometry (7), based (7), formalised (7), 2023 (7), main (7), agi (7), too (7), growing (7), entire (7), experience (7), wiles (7), forms (7), bloom (7), erdos (7), comes (7), days (7), worked (7), week (7), literature (7), step (7), knew (7), later (7), uses (7), key (7), following (7), unfortunately (7), access (7), student (7), nobody (7), hypothesis (7), once (7), little (7), released (7), possible (7), knowledge (7), exactly (7), saying (7), checking (7), designed (7), didn (7), without (7), test (7), claiming (7), great (7), anything (7), gets (7), property (7), terms (7), map (7), matter (7), call (7), peano (7), libraries (7), google (7), harmonic (7), further (7), assistant (7), undergrad (6), stuff (6), experiment (6), formalising (6), wants (6), fast (6), programming (6), nice (6), lie (6), feel (6), free (6), school (6), talks (6), explained (6), game (6), seem (6), trained (6), whose (6), talk (6), added (6), sometimes (6), tried (6), quickly (6), specific (6), developed (6), month (6), announcement (6), curves (6), modular (6), automorphic (6), asking (6), complete (6), becoming (6), containing (6), three (6), contain (6), second (6), six (6), amount (6), happened (6), philosophy (6), powers (6), couple (6), issues (6), fix (6), pretty (6), went (6), hours (6), universal (6), roby (6), defining (6), put (6), absolutely (6), nothing (6), turns (6), teach (6), explain (6), proved (6), lots (6), exciting (6), happening (6), world (6), types (6), putnam (6), hand (6), marking (6), interest (6), international (6), needed (6), style (6), ideally (6), class (6), pass (6), said (6), expensive (6), datasets (6), involving (6), fields (6), under (6), databases (6), technology (6), looking (6), integer (6), easy (6), needs (6), shortly (6), whatever (6), works (6), thank (6), solving (6), wrote (6), times (6), review (6), official (6), terence (6), missing (6), accelerate (6), required (5), 2026 (5), interactive (5), zulip (5), pages (5), push (5), functions (5), material (5), usually (5), opinion (5), essentially (5), future (5), contains (5), best (5), end (5), focus (5), longer (5), elliptic (5), line (5), mehta (5), evidence (5), latex (5), every (5), ultimately (5), breakthrough (5), today (5), cambridge (5), poor (5), known (5), expect (5), errors (5), manually (5), appendix (5), published (5), ones (5), concept (5), formalizing (5), short (5), satisfy (5), equal (5), worry (5), situation (5), less (5), ended (5), four (5), verified (5), publically (5), degree (5), sample (5), likely (5), performance (5), similar (5), having (5), advanced (5), score (5), whole (5), heard (5), reason (5), train (5), saw (5), money (5), testing (5), maybe (5), revealed (5), attempting (5), crack (5), classes (5), source (5), formally (5), often (5), unique (5), similarly (5), object (5), assumption (5), succ (5), tier (5), low (5), finding (5), involved (5), methods (5), languages (5), bytedance (5), yes (5), committee (5), scores (5), determined (5), silver (5), while (5), thomas (5), forum (5), hypotheses (5), approximately (5), wordpress (4), website (4), comment (4), report (4), sign (4), august (4), december (4), accelerating (4), posts (4), learn (4), including (4), web (4), program (4), coherent (4), others (4), growth (4), interested (4), online (4), user (4), gave (4), show (4), felt (4), january (4), life (4), focused (4), ever (4), easier (4), slow (4), taylor (4), funding (4), representations (4), finite (4), officially (4), looks (4), coming (4), led (4), hybrid (4), positive (4), must (4), arithmetic (4), video (4), giving (4), bhavik (4), months (4), personally (4), half (4), become (4), forward (4), maria (4), ines (4), track (4), important (4), reasons (4), conrad (4), berthelot (4), fine (4), lemma (4), left (4), twitter (4), list (4), intermediate (4), helping (4), play (4), abstract (4), rings (4), translated (4), compiles (4), basically (4), marks (4), guarantee (4), borcherds (4), order (4), accurate (4), reasoning (4), areas (4), mind (4), furthermore (4), checked (4), claimed (4), actual (4), secret (4), says (4), automatically (4), nontrivial (4), digit (4), typical (4), difficulty (4), suggests (4), failed (4), producing (4), came (4), description (4), soon (4), thoughts (4), close (4), 20th (4), internet (4), please (4), ploughing (4), fundamental (4), private (4), university (4), pattern (4), pure (4), college (4), institutions (4), hype (4), reporting (4), nonsense (4), motivated (4), construct (4), lift (4), true (4), congruent (4), choose (4), multiple (4), remember (4), running (4), isomorphism (4), uniquely (4), took (4), expected (4), category (4), sequences (4), build (4), itps (4), minutes (4), measuring (4), approaches (4), researcher (4), colleagues (4), task (4), frontier (4), invalid (4), assumptions (4), hallucination (4), various (4), doubt (4), boundary (4), day (4), announcing (4), mostly (4), seed (4), nature (4), scheme (4), across (4), worries (4), discussion (4), misformalization (4), previously (4), interaction (4), started (3), site (3), email (3), account (3), update (3), round (3), october (3), february (3), tensor (3), search (3), formalise (3), related (3), software (3), academic (3), team (3), development (3), developing (3), thanks (3), david (3), goal (3), support (3), offer (3), schoolchildren (3), difference (3), else (3), conference (3), generate (3), funded (3), capable (3), breaks (3), infrastructure (3), suggest (3), amazing (3), launched (3), backed (3), enabled (3), compile (3), obvious (3), ready (3), taking (3), blueprint (3), graph (3), spend (3), link (3), epsrc (3), stories (3), parts (3), analytic (3), graham (3), terry (3), submitted (3), contributed (3), weeks (3), third (3), final (3), quanta (3), term (3), announced (3), feasible (3), status (3), scholze (3), happy (3), magnitude (3), argue (3), arguments (3), seemed (3), whereas (3), pointed (3), power (3), book (3), concerned (3), false (3), confirmed (3), occasionally (3), moment (3), stress (3), flt (3), component (3), foundations (3), situations (3), cut (3), worth (3), makes (3), beat (3), hopefully (3), checker (3), submissions (3), riemann (3), claims (3), points (3), limited (3), grading (3), finish (3), elliot (3), weil (3), waiting (3), reddit (3), easily (3), early (3), article (3), quoted (3), precisely (3), random (3), succeed (3), trick (3), couldn (3), curated (3), quote (3), size (3), sentences (3), news (3), date (3), myself (3), broadly (3), variants (3), mathematically (3), send (3), allowed (3), necessary (3), thinks (3), efforts (3), perfect (3), direction (3), bros (3), firstly (3), looked (3), courses (3), offered (3), takes (3), move (3), universities (3), achieved (3), gauss (3), departments (3), literally (3), somehow (3), relation (3), constant (3), descends (3), produces (3), maps (3), yoga (3), version (3), called (3), calling (3), equivalent (3), words (3), stated (3), chosen (3), catch (3), infinite (3), run (3), lecturer (3), elements (3), scene (3), space (3), matters (3), analysis (3), proposed (3), finally (3), suggested (3), bottleneck (3), small (3), lines (3), increase (3), scale (3), classification (3), abilities (3), integration (3), successes (3), neural (3), networks (3), helpful (3), past (3), retrospect (3), sounds (3), learnt (3), entirely (3), guess (3), homework (3), sent (3), bespoke (3), alone (3), impossible (3), accessible (3), graduate (3), genuinely (3), accurately (3), involve (3), counterexamples (3), prize (3), unjustified (3), resolve (3), python (3), unable (3), ten (3), training (3), formula (3), aware (3), financial (3), social (3), unsolved (3), embargo (3), 28th (3), attempts (3), dolinar (3), explicitly (3), entries (3), possibly (3), determine (3), english (3), readable (3), especially (3), supposed (3), won (3), plausible (3), 707 (3), vibe (3), authors (3), distribution (3), collaboration (3), pro (3), kevin (3), guest (3), timescale (3), existing (3), beginning (3), particularly (3), 124 (3), thereafter (3), succeeded (3), manner (3), pipeline (3), person (3), careful (3), reductive (3), happen (3), prs (3), hallucinations (3), name (2), bar (2), view (2), content (2), log (2), subscribed (2), subscribe (2), march (2), uncategorized (2), tactics (2), rigour (2), m1f (2), algebraic (2), older (2), place (2), welcome (2), jump (2), preferred (2), chat (2), topics (2), developers (2), verification (2), roadmap (2), goes (2), tate (2), global (2), commutative (2), algebras (2), plan (2), differential (2), potential (2), flexible (2), application (2), interact (2), angle (2), highlights (2), yang (2), skeptical (2), side (2), thought (2), leancopilot (2), repository (2), spoke (2), presentation (2), viewed (2), 12th (2), scientists (2), projects (2), domain (2), file (2), presented (2), base (2), marked (2), foundation (2), richard (2), below (2), naturals (2), organisation (2), green (2), major (2), subgroups (2), rationals (2), due (2), collaborating (2), schemes (2), grant (2), conclusion (2), combinatorics (2), additive (2), unit (2), fractions (2), spectacular (2), patrick (2), massot (2), explanation (2), comprehensible (2), effective (2), upon (2), bounds (2), myers (2), exponential (2), improvement (2), refereed (2), previous (2), began (2), serious (2), biggest (2), breakthroughs (2), plus (2), logic (2), angeliki (2), appear (2), agreement (2), consider (2), error (2), smaller (2), justify (2), crucial (2), towards (2), themselves (2), arthur (2), ogus (2), him (2), response (2), stanford (2), module (2), develop (2), sci (2), tensor_a (2), products (2), closer (2), turned (2), desired (2), incorrect (2), suppose (2), funny (2), message (2), professional (2), anyway (2), weak (2), discovered (2), etc (2), practice (2), fixable (2), twist (2), grothendieck (2), directly (2), bluesky (2), fashioned (2), motivation (2), position (2), laid (2), role (2), relating (2), beautiful (2), gone (2), finished (2), sharing (2), envisage (2), smartest (2), entering (2), submitting (2), remind (2), vague (2), inaccurate (2), accept (2), super (2), success (2), whilst (2), talking (2), initial (2), excitement (2), glazer (2), confusing (2), apply (2), equivalently (2), information (2), surprised (2), shocked (2), setting (2), fail (2), throw (2), ace (2), expecting (2), remain (2), trust (2), correspond (2), creating (2), unlikely (2), understood (2), relatively (2), alpha (2), smart (2), struggle (2), imagine (2), quotes (2), challenging (2), rumour (2), spent (2), facts (2), secrecy (2), applications (2), feb (2), decent (2), interpreted (2), expressible (2), fancy (2), diagrams (2), explicit (2), typing (2), announce (2), skills (2), negative (2), produce (2), moving (2), thinking (2), tricked (2), behind (2), unrepresentative (2), generalise (2), intelligent (2), matching (2), london (2), theorist (2), reading (2), feed (2), drives (2), amused (2), redefined (2), unlike (2), equality (2), inductive (2), strange (2), aligns (2), surely (2), writes (2), confused (2), assume (2), coset (2), convenient (2), consequences (2), construction (2), normal (2), eats (2), quotientgroup (2), decided (2), stuck (2), associated (2), contrast (2), composing (2), isn (2), boiled (2), secretly (2), chose (2), 1000008 (2), 108 (2), perfectly (2), rely (2), fun (2), hidden (2), keep (2), canonical (2), curriculum (2), notes (2), never (2), ordered (2), archimedean (2), characterise (2), reals (2), characterises (2), usual (2), sergei (2), gukov (2), billions (2), 000 (2), milestone (2), requests (2), rigorous (2), helped (2), observations (2), brainstorming (2), hit (2), rate (2), changer (2), career (2), rapid (2), anger (2), flawed (2), naive (2), per (2), aimo (2), impressive (2), cost (2), lessons (2), mistakes (2), ouch (2), seconds (2), linked (2), mine (2), promising (2), majority (2), none (2), text (2), judge (2), correctness (2), remark (2), framework (2), applied (2), self (2), contained (2), applying (2), implicitly (2), phenomenon (2), stop (2), lose (2), dimension (2), gamma_0 (2), weight (2), obviously (2), readers (2), equation (2), zero (2), gives (2), gigantic (2), frustrations (2), generally (2), frustrated (2), closed (2), perform (2), harder (2), missed (2), media (2), million (2), miles (2), everything (2), extraordinary (2), extrapolate (2), summary (2), home (2), waited (2), unrefereed (2), chinese (2), against (2), scored (2), regarded (2), validate (2), truth (2), refereeing (2), closing (2), ceremony (2), contestants (2), collection (2), feeling (2), wait (2), cheat (2), capabilities (2), surprise (2), independently (2), wonderful (2), reported (2), bronze (2), translations (2), supply (2), translating (2), translation (2), value (2), smallest (2), corresponding (2), decide (2), precise (2), coordinators (2), markers (2), spoiler (2), alert (2), paid (2), return (2), despite (2), discussing (2), kinds (2), break (2), format (2), medals (2), kids (2), reasonable (2), namely (2), participants (2), 12ths (2), renaissance (2), philanthropy (2), institution (2), aim (2), raise (2), initative (2), scaling (2), fit (2), objects (2), alexeev (2), mixon (2), listed (2), agents (2), submit (2), includes (2), journal (2), lively (2), increasing (2), relative (2), contributions (2), activity (2), seeing (2), encourage (2), significant (2), regarding (2), experiences (2), realized (2), present (2), paul (2), formulated (2), death (2), slightly (2), trivial (2), meant (2), advantage (2), 480 (2), flipped (2), during (2), specifically (2), sufficiently (2), accordingly (2), changed (2), teams (2), modified (2), stijn (2), cambie (2), 488 (2), excited (2), selected (2), runs (2), successfully (2), change (2), auto (2), noticed (2), brief (2), fill (2), dustin (2), section (2), launch (2), include (2), nonetheless (2), accompanying (2), author (2), 2022 (2), oeis (2), links (2), boris (2), grow (2), organically (2), 10x (2), slop (2), trusted (2), connected (2), rare (2), acceleration (2), 2000 (2), representation (2), higher (2), design, loading, collapse, manage, subscriptions, reader, privacy, join, 203, subscribers, assistance, m4p33, m40001, m1p1, liquid, computability, categories, begin, installation, instructions, names, emerged, stay, topic, beginner, stream, members, plans, invite, consult, broad, vision, goals, enhancing, interface, functionality, cater, wide, range, users, engineers, modules, selmer, local, loeffler, michael, stoll, cebotarev, density, heather, macbeth, riemannian, manifolds, joining, textbook, widgets, presenting, graphical, hoping, interactively, schools, centre, equals, twice, circumference, subtleties, oriented, unoriented, angles, exposed, amazon, cedar, evgenia, karunus, anton, kovsharov, visualisation, kaiyu, maximally, dependency, bunch, totally, versions, 2029, paperproof, emina, torlak, flagship, contributing, 9th, showcased, plenty, thraine, christianson, documentation, static, enhanced, joachim, breitner, recursive, lang, live, hover, updates, warning, alex, fixes, leaff, tour, verso, port, organisations, nonprofit, simons, sloan, merkin, supporting, faster, adding, enhance, scott, morrison, tactic, lemmas, omega, hiring, convergent, familiar, blue, orange, colour, bifurcation, mazur, torsion, independent, route, eaten, september, body, flat, worried, awarded, unreasonable, amenable, technique, gowers, manners, document, summaries, katalin, marton, polynomial, freiman, ruzsa, progression, actively, yael, dillies, substantial, kelley, maka, planar, intention, 2019, smith, kaplan, goodman, strauss, aperiodic, monotiles, discusses, upper, ramsey, campos, griffiths, morris, sahasrabudhe, member, phenomenal, born, accrue, events, peter, ending, seminar, koutsoukou, argyraki, sorted, lets, documenting, documented, robust, withstand, knocks, chances, orders, formalists, doomed, properly, visited, berkeley, lunch, doc, 90s, promised, saved, meal, dug, hole, fixing, gossiping, mistake, telling, tadashi, tokieda, duly, brian, inbox, agreed, coffeeshop, islington, thesis, scratch, les, algebres, puissances, divisees, bull, 2ieme, serie, 1965, lemme, p86, repair, misquotes, 1963, ann, ens, gamma_a, gamma_r, accidentally, falls, stops, ring, cris, chambert, loir, frutos, fernandez, summer, irritating, complained, inspection, remarked, string, laughing, emojis, argued, tweeting, joined, yesterday, ignored, mentioning, trouble, observation, context, according, formalist, vanished, massive, collateral, damage, chunks, disappeared, books, vaporised, disappearance, practical, undoubtedly, 1970s, light, spoken, fuss, died, incomplete, temporary, 1990s, diamond, fujiwara, kisin, generalised, simplified, powerful, revolution, boundaries, 60s, 70s, paris, classical, logarithm, rham, characteristic, structures, 1960s, series, constructing, analogue, tedious, andrew, conditions, maintained, checkout, indication, dashboard, contribution, guidelines, barrier, rocq, isabelle, marker, verifies, convincing, carefully, grade, logical, dreading, inevitable, onslaught, middle, wade, hold, applicability, fully, solid, besides, performing, forces, worms, tempered, pressed, adjectives, simplest, brute, force, painful, involves, factoring, polynomials, parallelised, raises, representative, piece, revert, unsurprised, nearer, qual, describes, represent, mental, pre, sort, bright, schoolers, passing, ensure, innovative, recycling, unimpressed, answered, adequately, unattackable, basing, pay, fraction, valuable, desperately, frieder, depth, shortcomings, possess, definitive, computable, 9811, 367707, larger, guesswork, mapping, adically, continuous, iff, adic, valuation, 5th, bother, exact, figured, 4th, effort, suspect, tackled, expertise, outside, numerical, aren, 200, apparently, openly, frustrates, paragraph, rattle, paragraphs, pouring, fool, bets, slowing, explaining, sized, commence, advance, theorists, respond, nearby, nonnegative, mindless, stochastic, parrot, guessable, reports, spurious, contact, touch, crap, abysmal, invalidated, parroted, parrots, restricting, deluded, notion, oof, transpires, reportedly, sudden, sound, null, paraphrasing, regurgitate, analogous, sheets, encyclopedic, late, 1980s, 1960, top, stagnant, clogged, articles, sam, altman, refrain, air, linking, irresponsible, generation, nuts, stock, prices, internally, tells, commonly, adopted, nowadays, muddying, waters, allows, allow, containers, axiomatic, hood, triangle, commutes, characterising, constructions, subgroup, kernel, lifts, built, ploughed, upside, rfl, congruence, opaque, preimage, boils, composable, target, introduced, restate, diagonal, exists, parity, qed

Text of the page (random words):
nly temporary crystalline cohomology is in no practical sense wrong the theorems were still undoubtedly correct it s just that the proofs were as far as i am concerned incomplete or at least the ones antoine and maria ines were following were and unfortunately it is now our job to fix them the thing i want to stress is that it was absolutely clear to both me and antoine that the proofs of the main results were of course going to be fixable even if an intermediate lemma was false because crystalline cohomology has been used so much since the 1970s that if there were a problem with it it would have come to light a long time ago every expert i ve spoken to is in complete agreement on this point and several even went so far as to claim that i m making a fuss about nothing but perhaps they don t understand what formalization actually means in practice you can t just say i m sure it s fixable you have to actually fix it one added twist is that roby grothendieck and berthelot have all died so we could not go back to the original experts and ask directly for help for those that are interested in more technical details here they are berthelot s thesis does not develop the theory of divided powers from scratch he uses roby s les algebres a puissances divisees published in bull sci math 2ieme serie 89 1965 pages 75 91 lemme 8 on p86 of that paper seems to be false and it s not obvious how to repair the proof the proof of the lemma misquotes another lemma of roby from his 1963 ann sci ens paper the correct statement is gamma_a m tensor_a r gamma_r m tensor_a r but one of the tensor products accidentally falls off in the application this breaks roby s proof that the divided power algebra of a module has divided powers and thus stops us from defining the ring a_ cris so as i say antoine worked on fixing the problem whereas i just worked on gossiping about it to the experts and i made the mistake of telling tadashi tokieda about it in a coffeeshop in islington he duly went back to stanford and mentioned it to brian conrad and the next thing i knew conrad was in my inbox asking me what was all this about crystalline cohomology being wrong i explained the technical details of the issue conrad agreed that there seemed to be a problem and he went off to think about it several hours later he got back to me and pointed out that another different proof of the claim that the universal divided power algebra of a module had divided powers was in the appendix to the berthelot ogus book on crystalline cohomology and that as far as conrad was concerned this approach should be fine the proof was back on and that is pretty much the end of the story other than the fact that last month i visited berkeley and i had lunch with arthur ogus who i ve known since i was a post doc there in the 90s i d promised arthur a story of how he d saved fermat s last theorem and over the meal i told him about how his appendix had dug me out of a hole his response was oh that appendix has several errors in it but it s ok i think i know how to fix them this story really highlights to me the poor job which humans do of documenting modern mathematics there appear to be so many things which are known to the experts but not correctly documented the experts are in agreement that the important ideas are robust enough to withstand knocks like this but the details of what is actually going on might not actually be where you expect them to be for me this is just one of many reasons why humans might want to consider getting mathematics written down properly i e in a formal system where the chances of error are orders of magnitude smaller however most mathematicians are not formalists and for those people i need to justify my work in a different way for those mathematicians i argue that teaching machines our arguments is a crucial step towards getting machines to do it themselves until then we seemed to be doomed to fix up human errors manually the story does have a happy ending though two weeks ago maria ines gave a talk about formalization of divided powers in the cambridge formalization of mathematics seminar which was started by angeliki koutsoukou argyraki a couple of years ago thanks angeliki and my understanding of maria ines talk is that these issues have now been sorted out so we are actually back on track until the next time the literature lets us down posted in fermat s last theorem research formalisation tagged crystalline cohomology fermat s last theorem lean logic math mathematics maths peter scholze philosophy 20 comments lean in 2024 posted on january 20 2024 by xenaproject a huge amount happened in the lean theorem prover community in 2023 this blog post looks back at some of these events plus some of what we have to look forward to in 2024 modern mathematics i personally am a member of the lean community because of its phenomenal mathematics library mathlib which was born around six and a half years ago and has now become a very fast growing database of mathematics containing many but by no means all of the definitions used by modern research mathematicians today 2023 was the year where we really began to accrue evidence that formalisation of certain parts of serious modern mathematics is feasible in real time quanta s video on 2023 s biggest breakthroughs in mathematics talks about several results let s take a look at their status when it comes to formalisation in lean the first result in the quanta video is the result by campos griffiths morris sahasrabudhe giving an exponential improvement for upper bounds for ramsey numbers the previous post on this blog by bhavik mehta discusses his formalisation of the result he formalised the 50 page paper in five months before the paper had even been refereed the second result in the video is the work by smith myers kaplan and goodman strauss on aperiodic monotiles myers has developed enough of the theory of planar geometry to formalise the solution to a 2019 imo problem and announced earlier this week his intention to formalise the result in lean in 2024 the third and final result mentioned in quanta s round up was the kelley maka result on bounds for how big a set of positive integers must be before it must contain a 3 term arithmetic progression a formalisation of the result is being actively worked on by yael dillies they have made substantial progress however when it comes to formalising mathematics in real time we now have an even more spectacular data point terry tao led a team which formalised the main result in his breakthrough new paper with gowers green and manners proving katalin marton s polynomial freiman ruzsa conjecture the 33 page paper was formalised in just three weeks before the paper had even been submitted tao used patrick massot s lean blueprint software to make this web page which contains a latex lean hybrid document containing an explanation of the proof which is comprehensible to both a human and a computer he also made very effective use of the lean zulip with summaries posted every few days of what was ready to be worked upon ultimately 25 people contributed based on these and other stories coming out of the mathlib community one can come to the conclusion that there are parts of the modern theory of combinatorics and in particular additive combinatorics for which asking for a complete computer formalisation is not an unreasonable thing to do mehta and bloom also formalised bloom s proof of the erdos graham unit fractions conjecture which for me is evidence that some parts of analytic number theory are also becoming amenable to this technique fermat s last theorem however not all of modern mathematics is ready to be eaten by these systems for example in september i was awarded a grant by the epsrc the uk mathematics funding body to spend five years of my life formalising a proof of fermat s last theorem in lean lean has the definitions of elliptic curves and modular forms required to start us off but we are still working on other definitions such as automorphic representations finite flat group schemes and the like i cannot yet link to a blueprint because the project does not officially start until october 2024 and right now i m more worried about teaching my undergraduate lean course but i am part way through writing one and right now the graph looks like this people familiar with tao s blueprint graph will know that green means done and blue means ready to be done the new orange colour means a long way away already we see the first major bifurcation we need mazur s theorem on the torsion subgroups of elliptic curves over the rationals a huge project and completely independent of the theorems we ll need to push wiles ideas over the line the route we ll be taking is not the original wiles taylor wiles argument but a more modern one due to richard taylor who is collaborating with me on the mathematics of the project the focused research organisation in july 2023 the lean focused research organisation fro was launched focused research organisations are a new type of nonprofit for science backed by convergent research lean s fro is funded by the simons foundation sloan and richard merkin this has enabled a team of people to work full time on supporting the ever growing lean infrastructure and focus on many things such as making the mathematics library compile faster and adding infrastructure and tactics to enhance the user experience i give some examples below the fro is hiring by the way one example of the ways that the fro has made my own life easier scott morrison has developed omega for lean 4 a tactic for proving obvious to mathematicians lemmas about integers and naturals these things will no longer slow down my undergraduate students in fact july 2023 was an amazing month for the community because as well as the announcement of the fro it marked the end of the project to port all of lean s mathematics library from the now end of life lean 3 to lean 4 growing user base in computer science but let s get back to 2024 sometimes it felt to me that lean 3 was viewed as a tool for mathematics with its mathematics library the flagship project but both the fro and other researchers in computer science are contributing code and tools to make lean much more than this between 9th and 12th january 2024 the lean together 2024 conference showcased some of what was currently going on as well as talks by mathematicians on growing the mathematics library there were plenty of talks by computer scientists on tools or projects which they have been working on with lean for example david thraine christianson from the fro presented verso his domain specific language for documentation static blog posts such as tao s lean 4 proof tour can now be enhanced using this tool take a look at joachim breitner s blog post about recursive definitions on the lean lang web page this contains live code hover over it and the entire post was generated from a lean file if the language updates and the code breaks then a warning will be generated perhaps in the future infrastructure developed using alex best s leaff tool also presented at the conference could even be used to suggest fixes other non mathematical highlights for me at the conference emina torlak gave a presentation about how amazon are using lean in their cedar project evgenia karunus and anton kovsharov spoke about paperproof their visualisation tool for lean proofs which undergraduates seem to really like when i show it off in talks and kaiyu yang spoke about leancopilot an llm tool trained on lean s mathematics library whose main goal is to generate lean proofs i have always been skeptical of people who want to claim lean ai agi in fact i ve been maximally on the other side of the argument with my opinion being that llms are right now of essentially no use to me as a working mathematician but because i thought my undergraduates might like what i d seen in the talk i added leancopilot as a dependency for the repository i m using in my undergraduate course and it really can do a bunch of the problems sometimes in totally different ways to my model solutions i also tried it on a question someone asked on the lean zulip chat and it solved that too and quickly i think it will be interesting to see whether future versions of these tools will actually be of use to me in the fermat project i mentioned above which is funded until 2029 who knows what language models will be capable of then what else is to come in 2024 lean s widgets offer the user a very flexible way of presenting data in an interactive graphical way one application i am very much hoping that this year will be the year that i will be able to start doing high school level geometry interactively in lean i give talks in schools about the natural number game but i would like to write some new material about how to interact with statements such as angle at centre equals twice angle at circumference proving it using it in lean there are some subtleties here which are not usually explained to schoolchildren such as the difference between oriented and unoriented angles and which would be exposed by a formal approach as far as mathematics goes my team at imperial are currently working on tate modules selmer groups the local and global langlands program commutative algebra lie algebras and more when i start working full time on fermat s last theorem this will push the development of more of this kind of mathematics in lean there seems to be a coherent plan developing on the lean zulip for getting a basic theory of l functions formalised thanks to david loeffler michael stoll and others one natural goal would be results like cebotarev s density theorem used in fermat heather macbeth in 2023 formalised the definition of riemannian manifolds i feel like differential geometry is another area which now has huge potential for growth the fro have made it clear that they want to support this push for more mathematics in lean any mathematician interested in joining the community might want to start by working through the free online mathematics in lean textbook for plans in computer science related topics in 2024 i would invite you to consult the fro roadmap one thing i like about that page is the broad vision which the fro has one of the goals is enhancing its interface and functionality to cater to a wide range of users from mathematicians and software developers to verification engineers ai researchers and the academic community as always the lean community web pages are another place where people can begin to learn about lean including installation instructions and so on anyone who wants to try a fast interactive type based programming language for their project or who wants to formalise some mathematics is welcome to jump in and ask questions on the zulip chat full names are preferred and the two rules which have emerged in our community are stay on topic and be nice beginner questions are welcome in the new member...