Skip to content

Conversation

@cheukhei-chu
Copy link

@cheukhei-chu cheukhei-chu commented Nov 13, 2025

New files:

  • mellea/stdlib/reqlib/lean.py: new verifies for Lean 4 code
  • test/stdlib_basics/test_reqlib_lean.py: (incomplete) tests for some of the utility functions in lean.py
  • docs/examples/hilbert/hilbert.py: new Hilbert class containing utility functions for constructing proof generation workflow
  • docs/examples/hilbert/prove.py: customizable proof generation workflow using Hilbert class
  • docs/examples/hilbert/mathlib_retriever.py: (unfinished, work in progress) new Retriever class which is an implementation of a semantic Mathlib4 theorem retriever

@mergify
Copy link

mergify bot commented Nov 13, 2025

Merge Protections

Your pull request matches the following merge protections and will not be merged until they are valid.

🔴 Enforce conventional commit

This rule is failing.

Make sure that we follow https://www.conventionalcommits.org/en/v1.0.0/

  • title ~= ^(fix|feat|docs|style|refactor|perf|test|build|ci|chore|revert|release)(?:\(.+\))?:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant