Lean taskset: injected `axiom` bypasses the reward (#1271 `#print axioms` follow-up)

[dumko2001]

The lean_compiled reward accepts a proof when the protected signature is intact,
lake env lean exits 0, and there's no declaration uses 'sorry'. It never checks
the proof's axioms, so a rollout can prove any goal by injecting one:

import Mathlib
axiom cheat : False
-- DO NOT MODIFY the theorem statement below.
theorem fake_irrational : Irrational (1 : ℝ) := by
  exact cheat.elim

Irrational (1 : ℝ) is false. The axiom sits above the protected signature, so
the guard passes and the reward returns 1.0.

#1271 flagged this exact gap as future work; #1480 closed a sibling bypass in the
same reward.

Reproduction

Taskset image (Lean 4.27.0, Mathlib), exact lake env lean command:

proof body	compile	reward
axiom cheat : False + exact cheat.elim	exit 0, silent	1.0
sorry	declaration uses 'sorry'	0.0
axiom removed	unknown identifier	0.0

#print axioms fake_irrational → [cheat, propext, Classical.choice, Quot.sound].

Fix

#print axioms <name> after compile, reject axioms outside the trusted set. Ready
on a branch with a regression test. Two calls for you first:

• native_decide rests on Lean.ofReduceBool / Lean.trustCompiler — allow it
  (my default) or reject it as feat(lean): lean-guard markers + tamper-aware LeanRubric #1271 lists separately?
• The probe output needs last-match parsing like fix(lean-taskset): match LAST EXIT_CODE marker to close reward bypass #1480's EXIT_CODE, else a proof
  spoofs a clean line with #eval.

Can open the PR whenever it's useful.