From b03c3aec9d5b7b7f54bd7c1f39a3545f9ac3ed00 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 11:39:52 +0000 Subject: [PATCH 01/16] add file --- PreCFSG/Fitting.lean | 4 ++++ symptoms_of_ai_code.md | 8 ++++++++ 2 files changed, 12 insertions(+) create mode 100644 symptoms_of_ai_code.md diff --git a/PreCFSG/Fitting.lean b/PreCFSG/Fitting.lean index 708701e..186e260 100644 --- a/PreCFSG/Fitting.lean +++ b/PreCFSG/Fitting.lean @@ -103,6 +103,10 @@ lemma normal_map {G'} [Group G'] (H : Subgroup G) (φ : G ≃* G') : map_equiv_eq_comap_symm] exact normal_comap (φ : G →* G') +def com {G'} [Group G'] (φ : G →* G') : Subgroup G' →o Subgroup G where + toFun := comap φ + monotone' _ _ := comap_mono + /-- If `p : Subgroup G → Prop` is a property of subgroups of a group `G` that holds on a subgroup `H` if and only if it holds on the image of `H` under any automorphism of `G`, then the subgroup diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md new file mode 100644 index 0000000..f74f7f8 --- /dev/null +++ b/symptoms_of_ai_code.md @@ -0,0 +1,8 @@ +# Symptoms of AI Code + +This file collects what I identify as symptoms of AI code. +What I point out here need not be undesirable code, but could be. + +If carefully curated human code is the final goal of what AIs should write, then at least some of the items below need to be addressed! + +## From 048eb974a90e4435acfc4994f943030c4854c0f8 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:08:20 +0000 Subject: [PATCH 02/16] Walls of `have` and nested tactics --- symptoms_of_ai_code.md | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index f74f7f8..9bfa33e 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -5,4 +5,34 @@ What I point out here need not be undesirable code, but could be. If carefully curated human code is the final goal of what AIs should write, then at least some of the items below need to be addressed! -## +## Walls of `have` and forward reasoning + +* Disincentivize `have` +* Favor `refine`, `apply`, `exact` + +The rationale is that `have`s bloat the context for little gain. +Tactics like `refine` and `apply` have the opposite effect: +* they usually create more subgoals, +* the subgoals are good candidates for API lemmas (possibly with a filter that they should be separate goals, only if they require fewer/different assumptions to be proved) +* create a tree-like structure for the proof, which allows for "recursive solving" + +Using `refine` and `apply` often goes under the name of backward reasoning. + +Possible reason for so many auto-generated walls of `have`: +informal mathematics proof often "arrive at the conclusion" starting from the hypotheses. + +Imprecisely, if models could be trained by reading proofs from the end, they would likely begin with a `refine` or `apply` and generate as side-goals the latest `have`s. + +Continuing in this manner has better chances of writing more idiomatic code. + +It also highlights as possible API lemmas precisely the subgoals thus created. + +## Nested tactic calls + +`mathlib` has a loosely enforced principle that each line of a proof should contain at most one tactic. + +AI-generated proofs, however, often like interlacing tactic-mode proofs and term-mode proofs, by nesting `exact` with `by exact`, possibly multiple times. + +Disincentivising more than 1 tactic in each node of a sequence of tactics (a `tacticSeq`) seems more aligned with human code. + +The result is often more readable and more maintainable code. From 4f693592c2f9f938ea4a5dcfd02fcb4896d7fab8 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:12:47 +0000 Subject: [PATCH 03/16] reducing lengths of proofs --- symptoms_of_ai_code.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 9bfa33e..e335002 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -36,3 +36,11 @@ AI-generated proofs, however, often like interlacing tactic-mode proofs and term Disincentivising more than 1 tactic in each node of a sequence of tactics (a `tacticSeq`) seems more aligned with human code. The result is often more readable and more maintainable code. + +## Reduce lengths of proofs + +After getting familiar with formalisation, it becomes apparent that what seems like a single reasoning step, really hides multiple more atomic connections. + +AIs tend to take this to the extreme and produce individual proofs that are several hundreds or even thousands of lines long. + +Penalising proofs proportionally to their length may have the effect of splitting out (useful? see the "Walls of `have`" section) lemmas, improving performance, reducing the overall complexity by focusing on simpler results. From 66646d0e3fdb7319bc4ef78d83f53ad11951c381 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:16:06 +0000 Subject: [PATCH 04/16] numbers of defs --- symptoms_of_ai_code.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index e335002..00364e3 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -44,3 +44,13 @@ After getting familiar with formalisation, it becomes apparent that what seems l AIs tend to take this to the extreme and produce individual proofs that are several hundreds or even thousands of lines long. Penalising proofs proportionally to their length may have the effect of splitting out (useful? see the "Walls of `have`" section) lemmas, improving performance, reducing the overall complexity by focusing on simpler results. + +## Reduce the number of `def`initions + +While definitions are not intrinsically a symptom of bad code, many concepts do not actually need a separate definition. + +More definitions means writing more API for each definition, which in turn bloats the code-base for potentially little benefit. + +AI-generated proofs normally introduce multiple `def`initions for the most trivial of concepts. + +I think that it is worthwhile to seriously consider whether so many definitions are useful or harmful -- my inclination is to think that they are harmful. From 28af16e57c2e5750c62c694385e2fdd7e5faa55d Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:20:39 +0000 Subject: [PATCH 05/16] blueprints --- symptoms_of_ai_code.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 00364e3..0c1f33e 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -54,3 +54,13 @@ More definitions means writing more API for each definition, which in turn bloat AI-generated proofs normally introduce multiple `def`initions for the most trivial of concepts. I think that it is worthwhile to seriously consider whether so many definitions are useful or harmful -- my inclination is to think that they are harmful. + +## Writing and following a blueprint + +Human formalisation projects that have a blue-print are orders of magnitude more successful and efficient than projects that do not. + +Part of the reason is that the formalisation work can be distributed more efficiently and each step requires less specialised knowledge. + +However, another very important aspect is that a blueprint is an intermediate representation between the "fully informal" proof that humans consume and the very detailed and careful final formalised artifact. + +These intermediate "informalisation" steps should probably be studied more in detail and AI agents might even benefit from studying the edit-history of blueprints, to see what sort of adjustments are typical and possibly reproducible. From d9ffa7307870c10d732b0f5070ab9d12b1ad148c Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:23:29 +0000 Subject: [PATCH 06/16] review --- symptoms_of_ai_code.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 0c1f33e..38f42f0 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -64,3 +64,9 @@ Part of the reason is that the formalisation work can be distributed more effici However, another very important aspect is that a blueprint is an intermediate representation between the "fully informal" proof that humans consume and the very detailed and careful final formalised artifact. These intermediate "informalisation" steps should probably be studied more in detail and AI agents might even benefit from studying the edit-history of blueprints, to see what sort of adjustments are typical and possibly reproducible. + +## Review + +An efficient method for humans to improve their formalisation skills is being involved in the review process, both on the receiving end and on the reviewing end. + +AI-written code can similarly be reviewed by other AIs and the two could iterate on reviewing each others' code until it hopefully converges to a final state. From 6c4a3403ab5bf417c9d06fb90d7e37d1c69376ba Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:25:43 +0000 Subject: [PATCH 07/16] misformalisations --- symptoms_of_ai_code.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 38f42f0..dd6628c 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -70,3 +70,5 @@ These intermediate "informalisation" steps should probably be studied more in de An efficient method for humans to improve their formalisation skills is being involved in the review process, both on the receiving end and on the reviewing end. AI-written code can similarly be reviewed by other AIs and the two could iterate on reviewing each others' code until it hopefully converges to a final state. + +The reviewing process could also check for alignments between the informal notions and their formalised counterparts. This could help catch misformalisations, as well. From f6c139b0f1ed3c3953cee804f85f4364b9d9776d Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:30:05 +0000 Subject: [PATCH 08/16] generalisation --- symptoms_of_ai_code.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index dd6628c..aa4a70e 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -72,3 +72,11 @@ An efficient method for humans to improve their formalisation skills is being in AI-written code can similarly be reviewed by other AIs and the two could iterate on reviewing each others' code until it hopefully converges to a final state. The reviewing process could also check for alignments between the informal notions and their formalised counterparts. This could help catch misformalisations, as well. + +## Generalisation and adjustments + +After a result is formalised, humans normally look back at the process critically, looking for potential generalisation or rephrasing of lemmas. This fosters the creation of a more usable ecosystem. + +It might also be a place where previously duplicated code can now be seen as specialisation of a more general result, thus effectively *reducing* the code-base, while retaining the same expressivity. + +To me, this is one of the most important aspects of *progress*: achieving more simply, something that was previously hard. From 7da35a0f4274745653ef4578cedea08af96d7914 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:31:31 +0000 Subject: [PATCH 09/16] typo --- symptoms_of_ai_code.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index aa4a70e..f89c043 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -73,7 +73,7 @@ AI-written code can similarly be reviewed by other AIs and the two could iterate The reviewing process could also check for alignments between the informal notions and their formalised counterparts. This could help catch misformalisations, as well. -## Generalisation and adjustments +## Generalisations and adjustments After a result is formalised, humans normally look back at the process critically, looking for potential generalisation or rephrasing of lemmas. This fosters the creation of a more usable ecosystem. From edb2ced3922ead6743c5835ff19a07db774d6a73 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:36:42 +0000 Subject: [PATCH 10/16] revisiting old code --- symptoms_of_ai_code.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index f89c043..59948b6 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -80,3 +80,15 @@ After a result is formalised, humans normally look back at the process criticall It might also be a place where previously duplicated code can now be seen as specialisation of a more general result, thus effectively *reducing* the code-base, while retaining the same expressivity. To me, this is one of the most important aspects of *progress*: achieving more simply, something that was previously hard. + +## Revisiting old code + +This is a natural follow up to the step on generalisations. Once new code is streamlined, it is a good momento to look back at past code and see if it can benefit from the new additions. + +More code can do more stuff (often). + +However, real progress is when less code can do more stuff! + +Investigate periodically potential refactors that would not decrease the expressivity of the code-base, but would decrease its complexity, size or duplication should be a priority. + +No one gains from an incontrollable growth of code. From 1b5301ae3c5c1979fa2dce558722ccebda4a5572 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:37:30 +0000 Subject: [PATCH 11/16] typo --- symptoms_of_ai_code.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 59948b6..09c7eca 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -89,6 +89,6 @@ More code can do more stuff (often). However, real progress is when less code can do more stuff! -Investigate periodically potential refactors that would not decrease the expressivity of the code-base, but would decrease its complexity, size or duplication should be a priority. +Investigate periodically potential refactors that would not decrease the expressivity of the code-base, but would decrease its complexity, size or duplication. No one gains from an incontrollable growth of code. From 270290789be68fc7fa499b11fcff958c203034e3 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:39:50 +0000 Subject: [PATCH 12/16] typo --- symptoms_of_ai_code.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 09c7eca..f9a265f 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -91,4 +91,4 @@ However, real progress is when less code can do more stuff! Investigate periodically potential refactors that would not decrease the expressivity of the code-base, but would decrease its complexity, size or duplication. -No one gains from an incontrollable growth of code. +No one gains from uncontrollable code growth. From c9c2880ed148e3f7e41dd65b87642ce2f7c9df41 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 12:59:54 +0000 Subject: [PATCH 13/16] add tactics --- symptoms_of_ai_code.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index f9a265f..7a5e9ee 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -1,4 +1,4 @@ -# Symptoms of AI Code +# Quantifying Good Formal Proofs This file collects what I identify as symptoms of AI code. What I point out here need not be undesirable code, but could be. @@ -13,8 +13,9 @@ If carefully curated human code is the final goal of what AIs should write, then The rationale is that `have`s bloat the context for little gain. Tactics like `refine` and `apply` have the opposite effect: * they usually create more subgoals, -* the subgoals are good candidates for API lemmas (possibly with a filter that they should be separate goals, only if they require fewer/different assumptions to be proved) -* create a tree-like structure for the proof, which allows for "recursive solving" +* the subgoals are good candidates for API lemmas (possibly with a filter that they should be separate goals, only if they require fewer/different assumptions to be proved), +* create a tree-like structure for the proof, which allows for "recursive solving", +* tactic automation has more chances of helping with the side-goals. Using `refine` and `apply` often goes under the name of backward reasoning. From 036c97b9d56ac8ed9b63586ee65213c1811dcb46 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 13:12:10 +0000 Subject: [PATCH 14/16] add title --- symptoms_of_ai_code.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/symptoms_of_ai_code.md b/symptoms_of_ai_code.md index 7a5e9ee..8d8dd8d 100644 --- a/symptoms_of_ai_code.md +++ b/symptoms_of_ai_code.md @@ -1,4 +1,6 @@ -# Quantifying Good Formal Proofs +# Quality, Elegance, Discipline + +## Guidelines for AI‑Generated Formal Proofs This file collects what I identify as symptoms of AI code. What I point out here need not be undesirable code, but could be. From 3e4c98433cac2ef9ee23277d9091576520677603 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 13:12:36 +0000 Subject: [PATCH 15/16] rename to qed --- symptoms_of_ai_code.md => qed.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename symptoms_of_ai_code.md => qed.md (100%) diff --git a/symptoms_of_ai_code.md b/qed.md similarity index 100% rename from symptoms_of_ai_code.md rename to qed.md From 56a5f09bb38b1d0f7dc02203fbab785659a22c22 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Tue, 17 Mar 2026 13:14:08 +0000 Subject: [PATCH 16/16] deviations --- qed.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/qed.md b/qed.md index 8d8dd8d..3e33f7a 100644 --- a/qed.md +++ b/qed.md @@ -7,6 +7,8 @@ What I point out here need not be undesirable code, but could be. If carefully curated human code is the final goal of what AIs should write, then at least some of the items below need to be addressed! +I tried to focus on easily enforceable points, giving, where possible, a clear path to how to measure deviations. + ## Walls of `have` and forward reasoning * Disincentivize `have`