runqiwang777/tracer is a typed repair agent for Lean 4: it validates the proof candidates proposed by a model with the compiler and, when they fail, attempts repairs using error diagnostics and related examples. The repository description also lists the former name runqi-allen-wang/TRACER-Typed-Repair-Agent-with-Compiler-validated-Example-Retrieval. It is published under the MIT license, and no latest release is recorded in FACTS.
The completed run reported in the README covered 864 task attempts across 24 problems and repeated conditions for two model configurations. 811 of 864 (93.9%) passed within three attempts. The repository also includes a feature that replays the 24 cases and a benchmark of 254 historical repair tasks. This shows the tool does not merely generate proof candidates, but iterates the repair process based on compiler results.
That said, it has not been demonstrated that compiler feedback raises the success rate. In the README's direct comparison, runs with feedback matched the no-feedback retries in number of successes for Flash and were two cases lower for Pro out of 72 cases. The README states that larger studies require a full trace audit and independent recompilation before results are published. The current results are therefore closer to a test record awaiting additional validation than a confirmation of promising performance.