Newest at the top
| 2025-05-04 14:53:09 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 14:53:02 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 14:51:52 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-05-04 14:45:26 +0200 | <[exa]> | turns out I already classified it as such like 2 years ago :D |
| 2025-05-04 14:44:57 +0200 | <[exa]> | hellwolf: oh hvm is the thing with the "MAGIC" wannabe meme in the main readme |
| 2025-05-04 14:43:55 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 2025-05-04 14:42:42 +0200 | tremon | (~tremon@83.80.159.219) tremon |
| 2025-05-04 14:41:12 +0200 | haskellbridge | hellwolf go doing something relax too. enjoy your sunday folks |
| 2025-05-04 14:40:46 +0200 | <[exa]> | tomsmeding: np enjoy the sunday :D |
| 2025-05-04 14:40:28 +0200 | <haskellbridge> | <hellwolf> I know what you mean. But I will not be so quick to judge. |
| 2025-05-04 14:40:10 +0200 | <tomsmeding> | *sorry |
| 2025-05-04 14:40:05 +0200 | tomsmeding | is afk for a while, sory |
| 2025-05-04 14:39:53 +0200 | <[exa]> | hellwolf: I'd classify as scam tbh |
| 2025-05-04 14:39:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 14:39:28 +0200 | <haskellbridge> | <hellwolf> - bias of selling before confirmed result. |
| 2025-05-04 14:39:17 +0200 | <tomsmeding> | I see |
| 2025-05-04 14:39:01 +0200 | <tomsmeding> | and that sounds limited, but if you want something more than can be expressed to an engine like that, things become very hard, very undecidable, very quickly |
| 2025-05-04 14:38:52 +0200 | <[exa]> | tomsmeding: the issue is that my "instructions" won't very "simple" (usually multiple effects tied together), so just going the syntax way ("forth is instructions!") is going to be brutally bad |
| 2025-05-04 14:38:41 +0200 | <haskellbridge> | <hellwolf> https://x.com/VictorTaelin he is the frontman doing it. There is this VC vibe thing: so, there is sometimes selling before confirmation bias, but there are some interesting bits from time to time. I don't fully follow, tbh |
| 2025-05-04 14:38:18 +0200 | <tomsmeding> | and I mean, coding up a simple engine that tries to deduce a sequent from given ones with BFS isn't too hrad |
| 2025-05-04 14:37:20 +0200 | <tomsmeding> | [exa]: oh that definitely sounds like program synthesis :p |
| 2025-05-04 14:36:52 +0200 | <[exa]> | hellwolf: what's hvm and neogen? (googling leads to either twiddler or spam, which is sus) |
| 2025-05-04 14:35:31 +0200 | <[exa]> | and yeah well it's actually prolog. I want to write constraints on what holds "before" and should hold "after" the program, and the thing would ideally fill in some "middle" so that the "after" is satisfied. |
| 2025-05-04 14:35:19 +0200 | <haskellbridge> | <hellwolf> I think the hvm person is doing this entire neogen thing, banking on LLM model. |
| 2025-05-04 14:32:31 +0200 | <[exa]> | tomsmeding: I've just started reading up on the whole topic. Looks like I wanted more of a program synthesis. :D |
| 2025-05-04 14:31:23 +0200 | <[exa]> | hellwolf: if the heuristic is "there was more chat about it on the internet", it's going great. |
| 2025-05-04 14:26:50 +0200 | <haskellbridge> | <hellwolf> I wonder how well LLM nowadays to cope with these sort of things when it comes to heuristics |
| 2025-05-04 14:22:24 +0200 | <tomsmeding> | and do you want there to be proof search or just checking of manual proofs |
| 2025-05-04 14:21:47 +0200 | <tomsmeding> | what kind of things do you want to prove? |
| 2025-05-04 14:21:16 +0200 | <tomsmeding> | I mean you can actually model a proof checker, but at that point you're writing what you're asking already exists, I guess :p |
| 2025-05-04 14:16:02 +0200 | <[exa]> | s/List/Logic/ |
| 2025-05-04 14:15:19 +0200 | <[exa]> | tomsmeding: yeah like I could go full ListT but I guess it will need heuristics |
| 2025-05-04 14:14:12 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-05-04 14:11:57 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 14:05:46 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 14:04:14 +0200 | <tomsmeding> | prolog? |
| 2025-05-04 14:01:26 +0200 | <[exa]> | the issue with the theorem provers I see is that they kinda assume some particular fixed algebra (some kind of logic), I need some freedom in there without having to encode stuff too much. |
| 2025-05-04 13:58:47 +0200 | <[exa]> | s/if // |
| 2025-05-04 13:58:36 +0200 | <[exa]> | are there some good "small" libraries theorem proving? E.g. I've got an algebra, a few axioms on it, and I want to see how the axioms can be combined to derive some expression in the algebra. Ideally if axiom schemes are supported. |
| 2025-05-04 13:52:15 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 13:51:45 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 13:51:28 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 13:45:09 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 13:38:10 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 13:25:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 2025-05-04 13:16:15 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2025-05-04 13:13:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-05-04 13:08:16 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 13:07:59 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 13:07:29 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |