Show HN: Formal – Formal verification for AI-generated code using Lean 4(github.com)

4 pointsby yamafaktory3 เดือนที่ผ่านมา4 comments

Show HN: Formal – Formal verification for AI-generated code using Lean 4

https://github.com/yamafaktory/formal

6 comments

sjdv19823 เดือนที่ผ่านมา

I was initially very excited about this, but looking at the code: https://github.com/yamafaktory/formal/blob/4f95787ceeabb0f09...

To extract properties to verify... you call Claude??

yamafaktory3 เดือนที่ผ่านมา

Well, I can understand your frustration, but this is basically a pipeline that takes some code written by an LLM and attempts to prove its correctness using the Lean 4 theorem prover.

sjdv19823 เดือนที่ผ่านมา

How does your reply relate to my comment?

yamafaktory3 เดือนที่ผ่านมา

I'm sorry if it was unclear. My comment was just a validation of your assertion. It does use Claude - or any openai compatible LLM - to perform the extraction.

[deleted]3 เดือนที่ผ่านมา

angarrido3 เดือนที่ผ่านมา