Skip to content

Samarkand can be solved trivially by self-apply #145

Open

Description

@Marti2203

Hi,
I was trying out the game and it was really fun! But on level 8 I was a bit stumped as there was no hint and I saw that the goal theorem preimage_injective is available and tried applying it and it just worked? I am a little confused as to why that was allowed

Activity

  1. joneugster commented on Jul 3, 2026

    @joneugster
    Member

    Thanks. This is indeed a known big that needs to be fixed in lean4game.

  2. Marti2203 commented on Jul 3, 2026

    @Marti2203
    Author

    I'd be happy to try and figure out how to make a bugfix :) will try to spend some time next week on it

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions