You can cheat by hiding the LEM in a custom block

[roSievers]

If I hide the Law of Excluded Middle in a custom block, I'm able to use it in earlier levels which would also allow a proof without LEM.

To reproduce, wrap ((A→ ⊥) → ⊥) → A in a custom block and use it in the (((A → ⊥) → ⊥ ) → ⊥) → (A → ⊥) level.

[roSievers]

On a related note, I want to able to find out which axioms were assumed when constructing a block.

[nomeata]

If you are cheating, you are only cheating yourself :-)

I’m aware of this; the various levels just very thinly hide the additional basic rules, but the underlying logic is mostly the same.

I guess it would make sense for the system to track which axioms were used in each basic block, and gray out those not available in a certain task.

[roSievers]

Do the blocks remember their content, or is that forgotten, once the block is “compiled”?

[nomeata]

Right now, they are forgotten, but that is not necessary the final design.