{"author":"homarp","children":[{"author":"homarp","children":[{"author":"seunosewa","children":[{"author":"rawland","children":[{"author":"dominotw","children":[],"created_at":"2026-08-17T02:30:39.000Z","created_at_i":1786933839,"id":49325950,"options":[],"parent_id":49322873,"points":null,"story_id":49322330,"text":"so ' a problem' here is just preexisting math theorems ?","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T19:26:20.000Z","created_at_i":1786908380,"id":49322873,"options":[],"parent_id":49322822,"points":null,"story_id":49322330,"text":"There is one in the quickstart:

    mathcode -p "prove that the square of an even number is even"\n
\nhttps://math-ai-org.github.io/mathcode/#quickstart - if you look very closely, the screenshot at the top actually shows the output (and the solution).","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T19:20:10.000Z","created_at_i":1786908010,"id":49322822,"options":[],"parent_id":49322331,"points":null,"story_id":49322330,"text":"Could you provide a practical example?","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T18:17:10.000Z","created_at_i":1786904230,"id":49322331,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"A terminal AI coding assistant with a built-in math formalization engine \u2014 describe a problem in plain language and it converts it into a Lean 4 theorem and attempts a formal proof.","title":null,"type":"comment","url":null},{"author":"muds","children":[],"created_at":"2026-08-16T19:40:19.000Z","created_at_i":1786909219,"id":49322972,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?","title":null,"type":"comment","url":null},{"author":"owlbite","children":[{"author":"a2ff6eeb0","children":[{"author":"a2ff6eeb0","children":[{"author":"whattheheckheck","children":[{"author":"a2ff6eeb0","children":[],"created_at":"2026-08-17T11:47:12.000Z","created_at_i":1786967232,"id":49329358,"options":[],"parent_id":49326795,"points":null,"story_id":49322330,"text":"Effectively public domain.","title":null,"type":"comment","url":null}],"created_at":"2026-08-17T05:17:09.000Z","created_at_i":1786943829,"id":49326795,"options":[],"parent_id":49324972,"points":null,"story_id":49322330,"text":"Is this effectivly mit or no license?","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T23:43:42.000Z","created_at_i":1786923822,"id":49324972,"options":[],"parent_id":49323903,"points":null,"story_id":49322330,"text":"Or, more accurately: it's not possible to apply copyright to generated code; if you don't release it, it's a trade secret, but if you do, people can use it how they please.","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T21:31:39.000Z","created_at_i":1786915899,"id":49323903,"options":[],"parent_id":49323121,"points":null,"story_id":49322330,"text":"It's AI generated, so licensing terms are unenforceable.","title":null,"type":"comment","url":null},{"author":"jrflo","children":[{"author":"ljwoods2","children":[],"created_at":"2026-08-16T23:38:11.000Z","created_at_i":1786923491,"id":49324937,"options":[],"parent_id":49324066,"points":null,"story_id":49322330,"text":"Mathematics, Inc [1], I assume

[1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T21:50:54.000Z","created_at_i":1786917054,"id":49324066,"options":[],"parent_id":49323121,"points":null,"story_id":49322330,"text":"What commercial setting do you want to use a Lean theorem-proving agent in?","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T20:00:09.000Z","created_at_i":1786910409,"id":49323121,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.","title":null,"type":"comment","url":null},{"author":"eisbaw","children":[{"author":"bayesnet","children":[{"author":"wanderlust123","children":[{"author":"barrenko","children":[],"created_at":"2026-08-17T07:03:44.000Z","created_at_i":1786950224,"id":49327368,"options":[],"parent_id":49325539,"points":null,"story_id":49322330,"text":"+1","title":null,"type":"comment","url":null}],"created_at":"2026-08-17T01:14:35.000Z","created_at_i":1786929275,"id":49325539,"options":[],"parent_id":49325035,"points":null,"story_id":49322330,"text":"What kind of economic modelling uses Lean?","title":null,"type":"comment","url":null},{"author":"dominotw","children":[],"created_at":"2026-08-17T02:31:43.000Z","created_at_i":1786933903,"id":49325955,"options":[],"parent_id":49325035,"points":null,"story_id":49322330,"text":"do you have examples . i am fascinated by this","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T23:55:01.000Z","created_at_i":1786924501,"id":49325035,"options":[],"parent_id":49323278,"points":null,"story_id":49322330,"text":"I\u2019ve written a lot of Lean for economic modeling (so take this with the caveat that it\u2019s not frontier-level mathematics research) but I think this problem is overstated. If you follow good engineering standards\u2014keep primitives composable and design abstraction well\u2014it\u2019s 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\u2019re willing to make breaking changes all the time), so building on top of it makes life much easier.","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T20:19:49.000Z","created_at_i":1786911589,"id":49323278,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.","title":null,"type":"comment","url":null},{"author":"philipfweiss","children":[{"author":"fractorial","children":[{"author":"andxor","children":[{"author":"skew-aberration","children":[{"author":"cgio","children":[{"author":"skew-aberration","children":[],"created_at":"2026-08-17T03:35:19.000Z","created_at_i":1786937719,"id":49326312,"options":[],"parent_id":49325991,"points":null,"story_id":49322330,"text":"Nevertheless, the proof is valid and easy to certify","title":null,"type":"comment","url":null}],"created_at":"2026-08-17T02:39:47.000Z","created_at_i":1786934387,"id":49325991,"options":[],"parent_id":49325685,"points":null,"story_id":49322330,"text":"I am not sure of the premise. You can have a filter which takes garbage in and outputs the clean data from the garbage, a denoiser. Also your definition of slop is not specific to slop. Any input can be garbage, including this human sourced and thought comment.","title":null,"type":"comment","url":null}],"created_at":"2026-08-17T01:41:13.000Z","created_at_i":1786930873,"id":49325685,"options":[],"parent_id":49325082,"points":null,"story_id":49322330,"text":"Premises:\nGarbage in implies garbage out (first principle of computer science)\nThe input is possibly, but not necessarily garbage (definition of slop)

By the standard methods of modal logic, it follows that it is possible that the output is garbage and therefore slop by definition. QED.","title":null,"type":"comment","url":null}],"created_at":"2026-08-17T00:02:45.000Z","created_at_i":1786924965,"id":49325082,"options":[],"parent_id":49324124,"points":null,"story_id":49322330,"text":"> hooking up slop to slop is just unlikely to produce anything valuable

Do you have a formal proof of that?","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T21:58:40.000Z","created_at_i":1786917520,"id":49324124,"options":[],"parent_id":49323916,"points":null,"story_id":49322330,"text":"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 \u201cit compiles\u201d to \u201cit is correct\u201d before crystallizing them.","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T21:32:39.000Z","created_at_i":1786915959,"id":49323916,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"Maybe consider an integration with theoremdb.org?","title":null,"type":"comment","url":null},{"author":"dominotw","children":[],"created_at":"2026-08-17T02:29:42.000Z","created_at_i":1786933782,"id":49325947,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"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.","title":null,"type":"comment","url":null},{"author":"pullshark91","children":[],"created_at":"2026-08-17T04:44:55.000Z","created_at_i":1786941895,"id":49326633,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"My, what a creative name","title":null,"type":"comment","url":null},{"author":"c0rruptbytes","children":[],"created_at":"2026-08-17T07:19:50.000Z","created_at_i":1786951190,"id":49327438,"options":[],"parent_id":49322330,"points":null,"story_id":49322330,"text":"looks nice...time to turn it into a pi extension","title":null,"type":"comment","url":null}],"created_at":"2026-08-16T18:17:10.000Z","created_at_i":1786904230,"id":49322330,"options":[],"parent_id":null,"points":118,"story_id":49322330,"text":null,"title":"MathCode, Mathematical Coding Agent","type":"story","url":"https://math-ai-org.github.io/mathcode/"}