This is a trivial point, but is there a mistake in the statement?
We are assuming that n is even, and then multiplying by 2.

This Kata is not compatible with Lean v3.39.1 and needs to be upgraded.

This Kata is not compatible with Lean v3.39.1 and needs to be upgraded.

Approving the fork already merges.

Do I need to merge this change into the kata or is it resolved?

Approved

The line

notation `goldbach` := goldbach

in Preloaded causes a simple unfold goldbach / rw goldbach to fail. How might one work around this?

I believe this should be sorted, thanks.

Oops, sorry about this! I'll fix it now.

Please copy the content of Test Cases to Example Test Cases.

Edited, thanks

import category_theory.monad

I agree with monadius here. While kata based on the clever (ab)use of language features (such as the kata on embedding a stack-based language into Haskell mentioned in the Zulip chat) are most certainly welcome, there is a fine line between such clever kata and one that simply teaches how to break the system.

IMO the best course of action would be to unpublish this kata. If you discover loopholes within Codewars' Lean setup which can be (accidentally) bypassed and which cannot be defended against using a proper kata setup then feel free to report an issue on Codewars/codewars-runner-cli and we can see whether we can patch the loophole or otherwise find ways to detect such abuse automatically and mark them as cheats.

The description should clearly state that the goal of this kata is not to prove the given result but to pass tests by any means necessary. In general, it is a bad kata idea because it is possible to solve any Codewars kata by exploiting holes in test frameworks.