Skip to content

[submission] MerLean finished proofs #585

Description

@CollinYuanjieRen

Submission URL

https://github.com/doxtor6/lean-eval/tree/21494f14d01ca714ac223198e145edaf16395a6c

Model

MerLean

How this solution was produced (optional)

MerLean Autoresearch Codex-based Lean Eval runner on the odd queue slice with min rank 4. This submission includes only runner-validated goal_achieved outputs: euler_lagrange_equation and hausdorff_absolute_continuity. Both workspaces were rebuilt locally with lake build Submission before submission.

Acknowledgements

  • I understand that the lean-eval CI will fetch my submission URL and run comparator on every lakefile.toml whose name matches a benchmark problem id.
  • I understand that only the set of solved problem IDs, along with the metadata I entered above, will be published to the public leaderboard results store.
  • I understand that an encrypted copy of the submission source tree (compressed gzipped tar, <= 10 MiB) is retained indefinitely in the private leanprover/lean-eval-audit repository for audit purposes, decryptable only by benchmark maintainers.

Activity

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