fix: merge duplicate NewTheorem blocks (closes #25) by ZRTMRH · Pull Request #5 · AdamJasonKern/LinearAlgebraGame

ZRTMRH · 2026-05-17T23:38:14Z

Summary

lean4game silently keeps only the last NewTheorem block per level; earlier blocks are discarded (emitting the warning "You should only use one NewTheorem per level, but it takes multiple arguments").
Three levels had two NewTheorem blocks each, so the first block's theorems never appeared in the inventory and were unusable in proofs.
Merged each pair into a single NewTheorem call, placed after any helper lemma it references.

Levels fixed

Level	Theorems that were silently dropped
`InnerProductWorld/Level01`	`mul_le_mul_of_nonneg_right`, `div_mul_cancel`, `sq_eq_sq₀`, `sq_nonneg`
`InnerProductWorld/Level07`	`norm_zero_v`, `pythagorean`, `inner_self_nonneg`, `inner_self_eq_zero`, `sca_mul`, `ortho_decom`, `norm_nonneg_v`, `inner_zero_right_v`, `mul_le_mul_of_nonneg_right`, `div_mul_cancel`, `sq_nonneg`, `le_of_sq_le_sq`
`LinearIndependenceSpanWorld/Level08`	`Finset.sum_eq_sum_diff_singleton_add`, `Finset.smul_sum`, `inv_mul_cancel₀`

The L07 and L08 regressions were introduced by PRs #24 and #23 respectively, which appended a second NewTheorem instead of merging with the existing one.

Test plan

lake build succeeds (no new warnings introduced by this change)
Open InnerProductWorld Level 1: confirm mul_le_mul_of_nonneg_right, div_mul_cancel, sq_eq_sq₀, sq_nonneg are visible in the inventory panel and not greyed out
Open InnerProductWorld Level 7: confirm le_of_sq_le_sq and the other 11 previously-dropped theorems are visible, AND the 5 helper lemmas (norm_nonzero_of_nonzero, etc.) still appear
Open LinearIndependenceSpanWorld Level 8: confirm Finset.sum_eq_sum_diff_singleton_add, Finset.smul_sum, inv_mul_cancel₀ are visible alongside the two helper lemmas

🤖 Generated with Claude Code

This commit establishes a complete blueprint documentation system for the Linear Algebra Game, providing structured mathematical content for all game worlds: ## New Blueprint Content - **Tutorial World**: Basic tactics and proof techniques - **Vector Spaces**: Fundamental vector space properties and subspaces - **Linear Independence/Span**: Linear combinations, independence, and spanning sets - **Inner Products**: Inner product spaces, norms, orthogonality, and major theorems - **Linear Maps**: Linear transformations, null space, range, and fundamental properties ## Technical Improvements - Updated lean_decls file with 46 verified theorem declarations - Generated complete web documentation with dependency graph visualization - Established proper blueprint build system with leanblueprint integration - Created structured LaTeX source with modular chapter organization ## Features - Interactive dependency graph showing theorem relationships and proof status - Web-based documentation with LaTeX rendering and Lean code links - Comprehensive coverage of all implemented game worlds - Proper integration with existing Lean 4 codebase The blueprint provides both PDF and web versions, with the web version featuring an interactive dependency graph that visualizes theorem relationships and formalization status. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

…pdates This commit adds the missing LinearMapsWorld levels and updates throughout the game: ## New LinearMapsWorld Levels Added - **Level08**: Injectivity and Null Space (Axler 3.16) - injective maps have trivial null space - **Level09**: Injective Maps Preserve Independence - key property for understanding injectivity - **Level10**: Fundamental Theorem of Linear Algebra - basis definitions and dimension principles - **Level11**: Isomorphisms - bijective linear maps and structure preservation ## Game Content Updates - Updated InnerProductWorld Levels 06-08 with enhanced orthogonality and Cauchy-Schwarz content - Refined LinearIndependenceSpanWorld Level 07 with cleaner proof structure - Enhanced all LinearMapsWorld Levels 01-07 with improved hints and explanations - Updated TutorialWorld Level 10 and VectorSpaceWorld Level 05 with better pedagogy - Refreshed translation files (.i18n) with latest content ## Technical Verification - All 11 LinearMapsWorld levels build successfully with Lake - Complete progression from basic linear map definitions to advanced isomorphism theory - Proper dependencies and imports maintained throughout - Game.lean updated to reflect complete world structure This brings LinearMapsWorld to full completion with comprehensive coverage of linear map theory from Axler's "Linear Algebra Done Right". 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Corrected hint from `(one_smul (K := K) v).symm` to `(one_smul K v).symm` to match the working syntax used in the actual proof step. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

… levels This commit addresses collaborator feedback about game UX issues that were causing player confusion and game freezes. Systematic review revealed 11 total issues across 9 levels requiring fixes. ## Hint-Code Mismatch Fixes - **Variable naming**: Fixed funext default behavior (uses 'x' not 'v') in Level07 - **Curly brace syntax**: Removed incorrect {variable} syntax in hints across 5 levels - **Files**: Level03, Level06, Level07, Level09 (LinearIndependenceSpanWorld), Level04 (VectorSpaceWorld) ## Game Stalling Fixes - **Root cause**: Proofs ending with rewrites that create trivial goals need explicit rfl - **LinearIndependenceSpanWorld Level07**: Added rfl after final rewrite (original report) - **DemoWorld L01_HelloWorld**: Added rfl after rw[g] - **LinearMapsWorld Level06**: Added rfl after linear combination proof - **VectorSpaceWorld Level01**: Added rfl after rw[zero_add] ## Documentation Updates - **CLAUDE.md**: Added comprehensive game quality section with development guidelines - **Hint_Issues_Fixed_2025_07_26.md**: Detailed technical report of all fixes ## Impact - Prevents game freezing/stalling issues that frustrated players - Eliminates hint-code mismatches that caused confusion - Establishes best practices for future level development - Improves overall player experience significantly 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Remove rfl from VectorSpaceWorld Level01 (after rw[zero_add]) - Remove rfl from LinearMapsWorld Level06 (after rw[hT.2 a1 v1, hT.2 a2 v2]) - Remove rfl from LinearIndependenceSpanWorld Level07 (after rw[hf0 x hxs, hg0 x hxt]) - Update corresponding hints to match proof structure These rfl statements caused "no goals to be solved" compilation errors and framework stalling issues in lean4game interface. Proofs remain mathematically correct but now end with rewrite statements that lean4game can handle properly. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

…lay bugs - Fixed hint-code mismatches across multiple levels where hints showed incorrect syntax - Added 'Remember to add braces after by' reminders for have statements requiring `by { }` syntax - Fixed game stalling issues by adding stall warnings before problematic final proof steps - Added missing add_left_cancel theorem to VectorSpaceWorld Level01 Groups tab - Applied fixes to LinearIndependenceSpanWorld Level07, Level08, Level09 - Attempted workaround for Level 0 display bug in VectorSpaceWorld and LinearIndependenceSpanWorld - All fixes maintain working proof code while improving user experience 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

…LinearIndependenceSpanWorld **Problem**: Level 0 introduction pages showed blank content due to deep framework bug **Solution**: Created new Level01 introduction levels and shifted all existing levels up by 1 **VectorSpaceWorld Changes**: - Created new Level01 with comprehensive introduction to vector spaces - Shifted existing levels: Level01→Level02, Level02→Level03, ..., Level05→Level06 - Updated all imports and level numbers accordingly - Now has 6 levels total (01-06) **LinearIndependenceSpanWorld Changes**: - Created new Level01 with detailed introduction to linear independence and span - Shifted existing levels: Level01→Level02, Level02→Level03, ..., Level09→Level10 - Updated all imports and level numbers accordingly - Now has 10 levels total (01-10) **Benefits**: - Users can now access introductory content through a working Level 1 - No functionality lost - all original content preserved - Framework limitation bypassed without breaking existing gameplay - Both worlds now display introduction content properly **Build Status**: ✅ All levels compile successfully **Game Structure**: VectorSpaceWorld (6 levels) → LinearIndependenceSpanWorld (10 levels) → InnerProductWorld 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Changed numbered list (1. 2. 3. 4.) to bullet points (-) in 'The Mathematical Foundation' section - Resolves display parsing issue where numbered axioms were not rendering properly - Maintains consistent formatting with other bullet point sections - All four vector space axioms now display correctly 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Remove all .claude/ directories and their JSON configuration files - Clean up tdd-guard data files (modifications.json, todos.json, config.json) - Update i18n translation template (.pot file) - Remove embedded repository reference This cleanup removes development artifacts while preserving the core game functionality. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add lake exe cache get for faster builds - Add detailed logging and error checking - Add environment variable debugging - Exit on errors for clearer failure points 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Use Render's dynamic PORT environment variable - Remove set -e to allow continuing after non-critical failures - Add better error handling around lake build - Follow Render's port binding requirements 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Pre-build Lean project during Docker build instead of runtime - Simplify startup script to focus on server startup - Add fallback build if pre-build didn't work - Should resolve lake update hanging issues 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Copy dependency files first for better Docker layer caching - Use lake exe cache get --force for faster mathlib downloads - Improved .dockerignore to avoid build artifact conflicts - Dependencies only rebuild when lakefile.lean changes - Should dramatically reduce build times 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

… timeouts - Move npm install to Docker build phase for faster startup - Add fallback check in startup script if npm install didn't work - Should eliminate Render timeout issues during deployment - Runtime startup should now be under 30 seconds 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Use npm run build_client + npm run production instead of development mode - Eliminates concurrent processes (server + vite dev server) - Reduces memory footprint to fit within Render's 512MB free tier limit - Maintains all functionality while optimizing for cloud deployment 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Use complete 'npm run build' instead of just build_client - Use correct production entry point: relay/dist/src/index.js - Set proper NODE_ENV=production and PORT environment variables - Fix 'Cannot GET /' error by ensuring client/dist/ exists with proper routing 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

… issues - Build lean4game production bundle during Docker build (longer timeout) - Runtime only starts pre-built server (fast startup, low memory) - Eliminates both port scan timeout and memory limit issues - Optimal cloud deployment configuration 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- The deployed lean4game build script was missing build_relay - build_relay creates relay/dist/src/index.js needed for production - Run all three build steps: build_server, build_relay, build_client - This should create the complete production bundle 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Fixed 7 critical deployment issues identified through analysis: 1. ✅ Correct file path: Use relay/index.mjs (not non-existent relay/dist/src/index.js) 2. ✅ Use npm run production script instead of custom build paths 3. ✅ Build client at runtime (fast) vs complex build_relay step 4. ✅ Fix port binding: server now binds to 0.0.0.0 for external access 5. ✅ Simplified build process: pre-build server, runtime build client 6. ✅ Remove non-existent build_relay dependency 7. ✅ Use official lean4game production workflow This should eliminate all timeout, memory, and routing issues in one deployment. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Pre-build both server and client during Docker build (more memory available) - Remove runtime client build that was causing JavaScript heap out of memory - Server runs immediately with pre-built assets - Should resolve 404 errors from missing client/dist/ directory 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Create /home/node/lean4game/games/local/ directory - Symlink our LinearAlgebraGame to expected location - Resolves 'Did not find the following folder: /home/node/lean4game/games' error - Game should now be discoverable at https://linear-algebra-game.onrender.com 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add logging to check games directory structure at runtime - Verify symlink creation during Docker build - Debug why LinearAlgebraGame is not being discovered - Should help identify if symlink or game structure is the issue 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Set VITE_LEAN4GAME_OWNER=local to match games/local/ directory - Set VITE_LEAN4GAME_REPO=LinearAlgebraGame to match symlink name - Should enable direct access to LinearAlgebraGame in single-game mode - Game should now load at root URL https://linear-algebra-game.onrender.com 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Environment variables must be set during Vite build, not just runtime - Configure VITE_LEAN4GAME_SINGLE=true, OWNER=local, REPO=LinearAlgebraGame during build - Add environment variable logging for debugging - Should build client specifically for LinearAlgebraGame single-game mode 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Check game directory contents through symlink - Verify Game.lean accessibility - Debug exactly what lean4game server is seeing - Should help identify remaining configuration issues 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Single-game mode redirects to #/g/local/game (not LinearAlgebraGame) - Update VITE_LEAN4GAME_REPO=game to match expected URL - Update symlink from LinearAlgebraGame to game - Should resolve empty game page issue 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add LEAN4GAME_LOCAL_GAMES=true environment variable - lean4game was ignoring local games in production mode - Should enable discovery of games/local/ directory - Keep production mode for memory efficiency 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Experiment to test if adding LinearAlgebraGame to open statement allows players to use inner_self_eq_zero without the full namespace prefix. Changes: - Added LinearAlgebraGame to open statement in Level02 - Updated hints and proofs to use short names This may need to be reverted if it doesn't work on the game server. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

This reverts commit 04c9c53.

Improve spelling across game

Fix a small typo on Linear Independence and Span World Level 6.

Players could bypass the level by typing `apply sca_mul` since the Statement command makes the theorem available in the environment. Adding DisabledTheorem prevents this for the current level only. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

The fully qualified name DisabledTheorem alone only blocks `apply LinearAlgebraGame.sca_mul` but not `apply sca_mul`. Adding both forms to test if this covers the short name too. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

These theorems are used in the proof but were not listed in NewTheorem, so players couldn't see them in the theorem panel. Fixes #5 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…mpletion message, and proof simplification - InnerProductWorld Level 8: Add TheoremDoc and NewTheorem for inner_product_expansion and cross_term_bound, mention add_sq in Introduction - LinearMapsWorld Level 7: Replace premature "Congratulations on completing LinearMapsWorld!" with forward-looking message - LinearMapsWorld Level 5: Use linear_map_preserves_zero in non-empty proof and add it to sidebar Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Updated the README to reflect the new game title and added detailed game content, building instructions, and credits.

clarify nth_rw introduction

Level 10 introduces the `induction` tactic. The `Nat.add_succ` theorem was declared (TheoremDoc, NewTheorem) and mentioned in the Introduction, but the scripted proof uses `linarith` for the successor case — add_succ was never used, and it doesn't appear in any subsequent level either. Remove the orphaned declarations and Introduction paragraph to keep the level focused on its actual teaching goal (induction). Students who know add_succ can still use it — the game accepts any valid proof. Fixes #9 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

fix: introduce `sum_diff_eq_zero_of_equal_combinations`

- Move TheoremDoc for Set.union_subset from LinearIndependenceSpanWorld/Level07 to VectorSpaceWorld/Level05, alongside its NewTheorem. Previously the theorem fell into a namespace-default "Set" tab (with only itself) when first introduced, before its TheoremDoc was seen. Now it lands in "Sets" immediately. - In InnerProductWorld/Level03, unify tab names to the Unicode form used elsewhere in the world: "Real Numbers" → "ℝ" (3x), "Complex Numbers" → "ℂ" (2x). Eliminates side-by-side duplicate tabs for the same concept. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

Thanks, merged.

… (#19) * fix: replace duplicate Level 4 with null_space_is_subspace (closes #18) LinearMapsWorld Levels 2 and 4 both proved T 0 = 0 (issue #18). Level 5's intro promised a "null space is a subspace" result that didn't exist. This swaps Level 4's exercise to null_space_is_subspace and keeps linear_map_preserves_zero (used in Levels 5, 8, 9, 10) as a term-form helper := zero_in_null_space K V W T hT, since membership in null_space_v T is definitionally T 0 = 0. Removes the now-duplicate NewTheorem announcement of linear_map_preserves_zero from Level 5. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * doc: tighten Level 4 Conclusion Merge the two repetitive sentences into one and use the term "null space" instead of "the set of vectors that T sends to zero". Replace the vague "complete picture of how linear maps interact with subspace structure" trailer with a concrete forward-pointer to Level 5. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

…#22) The TheoremDoc and NewTheorem declarations advertised `inv_mul_cancel h` for proving `x⁻¹ * x = 1` from `h : x ≠ 0`, but in current mathlib that is `inv_mul_cancel₀` (the GroupWithZero version). Plain `inv_mul_cancel` is the group version and takes no hypothesis, so following the docs failed type-checking. Also simplifies the helper lemma's internal proof to use `inv_mul_cancel₀` directly instead of the indirect `mul_eq_one_iff_eq_inv₀` rewrite. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

…_union in Level 8 inventory (#23) Follow-up to #21: komugi64 reported that the helper lemma zero_coeff_from_not_in_span did not appear in the level's theorem inventory, forcing players to reprove it inline. Add TheoremDoc for both helpers and a second NewTheorem (placed after the lemma definitions, since NewTheorem resolves names at elaboration time) so they show up in the right-hand inventory panel. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

…enceSpanWorld L09 inventories (#24) Following up on the PR #23 fix for Level 8: an audit found the same pattern (helper lemmas defined and referenced in player-facing hints, but never registered with TheoremDoc/NewTheorem) in two more levels. InnerProductWorld Level 7 (Cauchy-Schwarz): - norm_nonzero_of_nonzero - norm_sq_decomposition - scaled_norm_le_original - norm_pos_of_nonzero - norm_sq_scaled_eq LinearIndependenceSpanWorld Level 9 (Span After Removing Elements): - union_diff_singleton_eq - fx_sum_equality - fw_sum_equality For Level 9, the helpers are defined above the existing NewTheorem, so we extend it in place. For Level 7, the existing NewTheorem precedes the helper definitions, so we add a second NewTheorem after them (same pattern as the Level 8 fix). All eight "No world introducing ..., but required by ..." build warnings for these helpers are eliminated. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

lean4game keeps only the last NewTheorem per level, silently dropping the earlier one. As a result, theorems listed in the first block were missing/disabled in the level inventory: - InnerProductWorld/Level01: mul_le_mul_of_nonneg_right, div_mul_cancel, sq_eq_sq₀, sq_nonneg were hidden. - InnerProductWorld/Level07: 12 theorems including le_of_sq_le_sq were hidden (added by PR #24 alongside the helper-lemma block). - LinearIndependenceSpanWorld/Level08: Finset.sum_eq_sum_diff_singleton_add, Finset.smul_sum, inv_mul_cancel₀ were hidden (regressed in PR #23). Each pair is merged into a single NewTheorem call, placed after any helper lemmas it references. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

ZRTMRH · 2026-05-17T23:38:26Z

Closing - wrong repo, will reopen on ZRTMRH/LinearAlgebraGame

ZRTMRH and others added 30 commits July 22, 2025 23:02

Add startup script for deployment

9bc3023

🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Fix Docker deployment: copy game files into container

9f18337

🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Fix port binding for deployment - bind to 0.0.0.0:3000

88d6a84

🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

ZRTMRH and others added 27 commits January 26, 2026 14:08

Revert "[TEST] Try open LinearAlgebraGame to allow short theorem names"

efac91b

This reverts commit 04c9c53.

fix: improve spelling across game

7163971

Merge pull request #1 from he7d3r/fix-typos

9f655ad

Improve spelling across game

Fix a small typo on Linear Independence and Span World Level 6.

778f3f6

Merge pull request #3 from Javantea/main

b6e6e16

Fix a small typo on Linear Independence and Span World Level 6.

Add missing inner_minus_left and inner_self_real to Level 6 sidebar

62c3d6f

These theorems are used in the proof but were not listed in NewTheorem, so players couldn't see them in the theorem panel. Fixes #5 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Add missing inner_zero_right_v to Level 7 sidebar

e366f88

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Revise README for Linear Algebra Game details

03b2460

Updated the README to reflect the new game title and added detailed game content, building instructions, and credits.

clarify nth_rw introduction

54902c8

Merge pull request #10 from JadAbouHawili/main

80c086e

clarify nth_rw introduction

doc: spacing for is_linear_combination

ce1c864

fix: introduce sum_diff_eq_zero_of_equal_combinations

2caf1ad

doc: fix inaccurate unfold tactic doc (#12)

361603a

make hypothesis name compatible with user choice (#11)

2c0778a

Merge pull request #14 from JadAbouHawili/spacing-docs

4aa9f91

fix: introduce `sum_diff_eq_zero_of_equal_combinations`

doc: remove unnecessary hint issues notes (#16)

4e0de03

Thanks, merged.

ZRTMRH closed this May 17, 2026

ZRTMRH deleted the fix/issue-25-merge-newtheorem-blocks branch May 17, 2026 23:38

Navigation Menu

fix: merge duplicate NewTheorem blocks (closes #25) - #5

fix: merge duplicate NewTheorem blocks (closes #25)#5
ZRTMRH wants to merge 107 commits into
AdamJasonKern:mainfrom
ZRTMRH:fix/issue-25-merge-newtheorem-blocks

ZRTMRH commented May 17, 2026

Uh oh!

ZRTMRH commented May 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

ZRTMRH commented May 17, 2026

Summary

Levels fixed

Test plan

Uh oh!

ZRTMRH commented May 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants