reuben364

2 tháng trướcdiscuss

The quote you gave seems reasonable on it's own. ICE and Palantir comes to mind as exactly the kind of thing one would want to avoid. Could you elaborate on what particularly you find lacking in that quote?

reuben364

6 tháng trướcdiscuss

I find that at the granularity you need to work with current LLMs to get a good enough output, while verifying its correctness is more effort than writing code directly. The usefulness of LLMs to me is to point me in a direction that I can then manually verify and implement.

reuben364

9 tháng trướcdiscuss

I was surprised to not see a connection made to free groups in the article.

EDIT: The wikipedia article that is.

reuben364

9 tháng trướcdiscuss

I'm working on formalizing https://arxiv.org/pdf/2508.18475 (A convex polyhedron without Rupert's property) in Lean4

I'm only on lemma 11 at this point, and up until that point the paper has been fairly easy to formalize (modulo my unfamiliarity with mathlib).

The repo is here https://github.com/badly-drawn-wizards/noperthedron

reuben364

năm ngoáidiscuss

I'm wondering whether such syntax is subsumed by something like Lean 4 macros. I believe Lean 4 already treats binders specially in its syntax for macro hygiene reasons, but I'm not confident in that assertion.

reuben364

năm ngoáidiscuss

Since the de Bruijn indices are limited (and presumably still Turing complete), I wonder how limited you can make them and still be Turing complete.

reuben364

năm ngoáidiscuss

I just wrote redef to emphasize that I'm not shadowing the original definition.

    def a := 1
    def f x := a * x
    -- at this point f 1 evaluates to 1
    redef a := 2
    -- at this point f 1 evaluates to 2

But with dependent types, types can depend on prior values (in the previous example the type of x depends on the value t in the most direct way possible, as the type of x is t). If you redefine values, the subsequent definitions may not type-check anymore.

reuben364

năm ngoáidiscuss

Thinking out aloud here.

One pattern that I have frequently used in EMACS elisp is that redefining a top-level value overwrites that value rather than shadowing it. Basically hot reloading. This doesn't work in a dependently typed context as the type of subsequent definitions can depend on values of earlier definitions.

    def t := string
    def x: t := "asdf"
    redef t := int

redefining t here would cause x to fail to type check. So the only options are to either shadow the variable t, or have redefinitions type-check all terms whose types depend on the value being redefined.

Excluding the type-level debugging they mention, I think a lean style language-server is a better approach. Otherwise you are basically using an append-only ed to edit your environment rather than a vi.

reuben364

năm ngoáidiscuss

There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (including lemmas and theorems).

reuben364

năm ngoáidiscuss

It matters for anti-circumvention, where they can go after people that make tools that allow you to make personal copies.

reuben364

2 năm trướcdiscuss

Not sure of details to make it a mathematical foundation but:

A category can be defined in terms of its morphisms without mentioning objects and a topos has predicates as morphisms into the subobject classifier.

reuben364

2 năm trướcdiscuss

That'd almost be partial functions with extra steps. Take the Klesili category with the Maybe Monad,and you get partial functions.

Unless you are manually matching on the the Maybe, and thus observing the timeout, then that isn't the case. You'd probably also want a nondetermism effect which cannot handle unless you specifically build your timeouts to be deterministic, which I think Lean 4 does, but you can't go from partial to total with it afaik.

reuben364

2 năm trướcdiscuss

a function will return to it's call site (or diverge), a handler doesn't necessarily have to resume from where it was invoked. There is also (sort of) dynamic scoping, where you don't have to thread the handlers through calls.

reuben364

2 năm trướcdiscuss

I'm left confused as to what the gluing in the rule replacement is. Must the boundary of a rule match on both sides? Also what examples there would be of what an example would of having topology that is not induced from a graph if it is at all possible.

reuben364

2 năm trướcdiscuss

I didn't expect Lean 4 in this context.

reuben364

2 năm trướcdiscuss

At first glance that does seem to match my temperament. I love this quote as I have recently discovered it working for me

  If you want to think clearly, be calm and be smart; schedule a Micro Nervous Breakdown at least once a day.

not sure if that is healthy though.

I guess with regards to mental health DSM type issues vs other issues, it is difficult to untangle for me. It may not be an actual disorder, but it certainly causes me distress. It's like being a science enthusiast that can't move past reading pop-sci articles (but wants to).

reuben364

2 năm trướcdiscuss

On medication for ADHD, it helps in the short term, but I still struggle to commit to working on things in the long term. I either get bored or forget or find a new shiny.

My job involves static analysis and I have an interest in PLT, so I've found some papers (Abstracting Abstract Machines) that I'll read through and get a rough idea. But to truly understand things I have to implement the ideas, but the scope of what I want to do expands so fast that I get demotivated and eventually move on.

Categories for the working mathematician, Software Foundations, contributing to mathlib are all things that I sort of start working towards and cannot force myself to get to any meaningful conclusion. At the same time starting so many things is how I slowly accumulated the foundations necessary to even approach these things.

It doesn't help that I also have PDA autism, which leads any sort of structure I try to impose on myself eventually becoming too stressful. I feel like I've reached the extent that modern medicine (I'm just short of max dosage of XR Ritalin) and therapy I can afford can help me.

reuben364

3 năm trướcdiscuss

Don't get me wrong, I agree, but aren't all solutions to problems situated in reality conterfactual to some degree. To the extent of my knowledge, isn't it all deterministic. To enact a stategy is to presume a free agent, individual or collective, acts according to that strategy. The act of communicating that strategy is in essence to convince those interests align with the outcome to act accordingly. We deal with imperfect information, it could be possible that someone, or a small group can unilaterally disseminate a strategy that drives wider cooperation, but those are probably unknown unknowns far too complicated to decipher by any cooperating party.

Of course this isn't it. Warp drives and luxury space communism seem to be something we could only stumble into.

reuben364

3 năm trướcdiscuss

With my limited knowledge, I don't see it. Could you elaborate on how you made that connection?

reuben364

3 năm trướcdiscuss

I'm having trouble getting the types right for the formula mentioned under the Matrix Function heading. Is f meant to be linear? Is f' meant to be pointwise derivative?

Submissions

Show HN: Paragrai – add paragraphs to badly formatted web novel translations

comments