Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / imperialcollegelondon/natural_number_game issues and pull requests
#134 - improper solution to level 6/9 (uses zero_ne_succ)
Issue -
State: closed - Opened by rmcmanus342 3 months ago
- 1 comment
#133 - 'generalizing' is locked at the level it is being introduced.
Issue -
State: open - Opened by zadeoglu 9 months ago
#132 - nicer proof for level13.lean
Pull Request -
State: open - Opened by abourque72 11 months ago
#131 - Tutorial world, Level 4, one single "refl," causes "Proof complete!"
Issue -
State: open - Opened by liusida about 1 year ago
#130 - Update level1.lean
Pull Request -
State: open - Opened by abuseofnotation about 1 year ago
#129 - unknown identifier 'not_iff_imp_false' error on Level 15 in the Inequality world
Issue -
State: open - Opened by roozbeh-yz over 1 year ago
#128 - Fix missing word in intro.lean
Pull Request -
State: open - Opened by vezwork over 1 year ago
#127 - Change name order
Pull Request -
State: closed - Opened by Anoushka1406 over 1 year ago
- 1 comment
#126 - Advanced Addition World - Level 10 and 11
Issue -
State: open - Opened by miguel-negrao almost 2 years ago
- 2 comments
#125 - recursion break
Issue -
State: open - Opened by orhid about 2 years ago
- 2 comments
#124 - Some Complaints
Issue -
State: open - Opened by EnderGZM about 2 years ago
- 1 comment
#123 - A typo in "Advanced Addition World Level 5" (inconsistent variable name)
Issue -
State: open - Opened by Kaiwen-S over 2 years ago
#122 - fix typo on level 6-7
Pull Request -
State: closed - Opened by Stevenjin8 over 2 years ago
#121 - Minor typo in World 10 Lvl 1
Issue -
State: open - Opened by milescalabresi almost 3 years ago
#120 - Improve wording in multiplication distributivity lemmas
Pull Request -
State: closed - Opened by chezbgone almost 3 years ago
#119 - Added german translation
Pull Request -
State: open - Opened by Lelidle almost 3 years ago
#118 - "What next?" page
Issue -
State: open - Opened by jcommelin about 3 years ago
#117 - Advanced Proposition World LV10 bug
Issue -
State: closed - Opened by micmelesse about 3 years ago
#116 - website down
Issue -
State: closed - Opened by micmelesse about 3 years ago
- 3 comments
#115 - Fix typo in world5, level6
Pull Request -
State: open - Opened by gruhn about 3 years ago
#114 - A motley collection of Corrections, Complaints and (Curious) Suggestions
Issue -
State: open - Opened by ghost over 3 years ago
#113 - Added "import tactic.tauto -- useful high-powered tactic"
Pull Request -
State: closed - Opened by hmonroe over 3 years ago
#112 - reward for finishing
Issue -
State: open - Opened by kbuzzard over 3 years ago
#111 - inductive le world?
Issue -
State: open - Opened by kbuzzard over 3 years ago
#110 - nth_rewrite
Issue -
State: open - Opened by kbuzzard almost 4 years ago
#109 - Update level1.lean
Pull Request -
State: open - Opened by vihdzp almost 4 years ago
#108 - save your game
Issue -
State: open - Opened by kbuzzard almost 4 years ago
#107 - Explain 'B_of_A' naming convention for implications 'A->B'
Issue -
State: open - Opened by davidblitz almost 4 years ago
- 1 comment
#106 - typo in multn world 1/9
Issue -
State: open - Opened by kbuzzard almost 4 years ago
#105 - Unable to use and_symm theorem in World 7, Level 3
Issue -
State: open - Opened by Gunjeet-Singh about 4 years ago
#104 - Bug in first two levels of the Power World
Issue -
State: closed - Opened by czAdamV about 4 years ago
- 1 comment
#103 - How to apply Leibniz's law for equality?
Issue -
State: open - Opened by darijgr about 4 years ago
- 3 comments
#102 - Undocumented implicit variables in Advanced Addition World
Issue -
State: open - Opened by darijgr about 4 years ago
#101 - Add ability to toggle between rendered view and literal lean
Issue -
State: open - Opened by al-yisun about 4 years ago
#100 - Shorten the proof of not_succ_le_self.
Pull Request -
State: closed - Opened by Julian about 4 years ago
- 1 comment
#99 - Some solutions use `assumption` which isn't mentioned in the text
Issue -
State: open - Opened by Julian about 4 years ago
#98 - Mark things as irreducible?
Issue -
State: open - Opened by shingtaklam1324 over 4 years ago
#97 - fold away hints
Issue -
State: open - Opened by kbuzzard over 4 years ago
#96 - Typo in world 3 level 1
Issue -
State: open - Opened by baldoalessandro over 4 years ago
#95 - Tutorial world fully translated to French
Pull Request -
State: open - Opened by ADedecker over 4 years ago
#94 - world 7 level 8 "did you spot the import?"
Issue -
State: open - Opened by kbuzzard over 4 years ago
#93 - Reuse the proof from the solution to level 16
Pull Request -
State: open - Opened by eric-wieser over 4 years ago
#92 - World 10, level 16: Simplify the proof even further, using an earlier result
Pull Request -
State: open - Opened by eric-wieser over 4 years ago
#91 - Sian Carey fellowship
Issue -
State: open - Opened by kbuzzard over 4 years ago
#90 - More French translation
Pull Request -
State: closed - Opened by sgouezel over 4 years ago
#89 - explain implicit inputs
Issue -
State: open - Opened by kbuzzard over 4 years ago
#88 - Advanced Proposition world: Level 1/10
Issue -
State: closed - Opened by arademaker over 4 years ago
- 1 comment
#87 - Drop down menu for levels
Issue -
State: closed - Opened by pglutz over 4 years ago
- 2 comments
#86 - Update level1.lean
Pull Request -
State: closed - Opened by arademaker over 4 years ago
#85 - Update level1.lean
Pull Request -
State: closed - Opened by arademaker over 4 years ago
- 1 comment
#84 - props aren't decidable in world 7
Issue -
State: open - Opened by kbuzzard over 4 years ago
#83 - French translation stub (home page and level 1)
Pull Request -
State: closed - Opened by PatrickMassot over 4 years ago
- 1 comment
#82 - The lines "-- World name : ..." removed
Pull Request -
State: closed - Opened by mpedramfar over 4 years ago
- 3 comments
#81 - add basic stuff about primes
Issue -
State: open - Opened by kbuzzard over 4 years ago
Labels: enhancement
#80 - add odd and even numbers
Issue -
State: open - Opened by kbuzzard over 4 years ago
Labels: enhancement
#79 - Add `not_iff_imp_false` to Advanced Proposition/Level 9
Pull Request -
State: closed - Opened by shingtaklam1324 over 4 years ago
- 1 comment
#78 - eq_zero_of_add_right_eq_self
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#77 - Fix typo on world1/level1.lean
Pull Request -
State: closed - Opened by crunsk over 4 years ago
- 1 comment
#76 - Advanced Addition World, Level 11: add_right_eq_zero
Issue -
State: closed - Opened by trj2059 over 4 years ago
- 1 comment
#75 - Fix typo in world7/level5.lean.
Pull Request -
State: closed - Opened by obi1kenobi over 4 years ago
- 2 comments
#74 - nat versus mynat issue with literal zeros
Issue -
State: closed - Opened by gjm11 over 4 years ago
- 2 comments
#73 - Save progress
Issue -
State: closed - Opened by rudolfovic over 4 years ago
- 7 comments
#73 - Save progress
Issue -
State: closed - Opened by rudolfovic over 4 years ago
- 7 comments
#72 - Use only x and y variables in world1 level 2
Pull Request -
State: closed - Opened by ben-dyer over 4 years ago
- 1 comment
#71 - not_succ_le_self better solution
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#70 - Remove an extraneous rewrite.
Pull Request -
State: closed - Opened by postmasters over 4 years ago
- 1 comment
#69 - Fix the application of `add_right_eq_zero`
Pull Request -
State: closed - Opened by postmasters over 4 years ago
- 1 comment
#68 - Description ahead of `succ_inj'`
Issue -
State: closed - Opened by stanescuUW over 4 years ago
- 1 comment
#67 - Lean can get stuck an infinite loop
Issue -
State: closed - Opened by FreeFull over 4 years ago
- 1 comment
#66 - fix broken link to Maths_Challenges
Pull Request -
State: closed - Opened by bryangingechen over 4 years ago
#65 - "unknown identifier 'not_iff_imp_false'" error in Advanced Proposition Level 9
Issue -
State: closed - Opened by edderiofer over 4 years ago
- 3 comments
#64 - hacker news UX comments
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#63 - Advanced muit world level 4 revert
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 2 comments
#62 - Night Mode
Issue -
State: open - Opened by ericrbg over 4 years ago
- 4 comments
Labels: help wanted
#61 - \l and \1
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#60 - it's hard to find this repository
Issue -
State: closed - Opened by robx over 4 years ago
- 3 comments
Labels: documentation
#59 - Fix note about using have in world 10 level 7
Pull Request -
State: closed - Opened by tyilo over 4 years ago
- 1 comment
#58 - Fixed missing quote for monospace formatting
Pull Request -
State: closed - Opened by zx9w over 4 years ago
- 1 comment
#57 - basic tactics file
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#56 - old notes
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 3 comments
#55 - possibly missing levels
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 3 comments
#54 - decidability
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#53 - 25 rewrites not 27 for (a+b)^2
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#52 - comments for experts?
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#51 - "end credits"
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 1 comment
#50 - Submitting simplified proof for level 10.16
Pull Request -
State: closed - Opened by ahelwer over 4 years ago
#49 - inconsistent letters between the text description and the formal theorem statement in Advanced Addition world level 6
Issue -
State: closed - Opened by ghost over 4 years ago
- 1 comment
#48 - contrapositive not proved?
Issue -
State: closed - Opened by kbuzzard over 4 years ago
- 7 comments
#47 - Two small fixes
Pull Request -
State: closed - Opened by MatthiasHu over 4 years ago
#46 - binomial theorem?
Issue -
State: open - Opened by kbuzzard almost 5 years ago
- 1 comment
Labels: enhancement
#45 - sandbox
Issue -
State: closed - Opened by kbuzzard almost 5 years ago
- 1 comment
#44 - pow_succ typo
Issue -
State: closed - Opened by kbuzzard almost 5 years ago
- 1 comment
#43 - email
Issue -
State: closed - Opened by kbuzzard almost 5 years ago
- 1 comment
#42 - Match lean file path with latest online game.
Pull Request -
State: closed - Opened by ghost almost 5 years ago
#41 - LEUNG Donald Sebastian blog comments
Issue -
State: closed - Opened by kbuzzard almost 5 years ago
- 1 comment
#40 - Fixed small typo with problem description for world4 level5
Pull Request -
State: closed - Opened by thyrgle almost 5 years ago
#39 - Please fix error in pow level description
Pull Request -
State: closed - Opened by ikrukov almost 5 years ago
- 1 comment
#38 - Update level13.lean
Pull Request -
State: closed - Opened by 3abc almost 5 years ago
- 1 comment
#37 - Update level3.lean
Pull Request -
State: closed - Opened by 3abc almost 5 years ago
- 1 comment
#36 - Lean server fails to initialize correctly in Safari 13.0.3 on macOS Catalina 10.15.1
Issue -
State: closed - Opened by DonaldKellett almost 5 years ago
- 4 comments