Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • sounds like an awesome project.

    wish these project always start with an example. i dont care about quickstart or featurelist if i dont know what this is.

    by dominotw
  • looks nice...time to turn it into a pi extension
    by c0rruptbytes
  • Maybe consider an integration with theoremdb.org?
    by philipfweiss
  • To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.

    Value is in how maths is communicated: The process, frustrations, triumphs, etc.

    We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them.

    by fractorial
  • Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
    by owlbite
  • It's AI generated, so licensing terms are unenforceable.
    by a2ff6eeb0
  • What commercial setting do you want to use a Lean theorem-proving agent in?
    by jrflo
  • A terminal AI coding assistant with a built-in math formalization engine — describe a problem in plain language and it converts it into a Lean 4 theorem and attempts a formal proof.
    by homarp
  • Could you provide a practical example?
    by seunosewa
  • the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
    by eisbaw
  • I’ve written a lot of Lean for economic modeling (so take this with the caveat that it’s not frontier-level mathematics research) but I think this problem is overstated. If you follow good engineering standards—keep primitives composable and design abstraction well—it’s not so hard to understand enough Lean to ensure the formalized statement is correct.

    In part this is possible because mathlib is very well-designed and has a very good API (in no small part because they’re willing to make breaking changes all the time), so building on top of it makes life much easier.

    by bayesnet
  • Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
    by muds