sibrahim

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical.

Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments.

So, if you have a formal statement that you've verified to represent what you are interested in by some other means, Lean can tell you whether the proof created by genAI is correct. Basically, there is a nigh infallible checker that won't accept incorrect hallucinations.

It depends on whether you are doing something security critical with the result.

Maybe you have a trusted table hash but only a user-supplied version of the table. Before you use that data for security sensitive queries, you should verify it hasn't been modified.

Basically, if you ever have to contend with a malicious adversary, things are more interesting as usual. If not, addition is likely fine (though 2^k copies of a row now leave the k lowest bits unchanged).

XOR is not a great choice here. Consider that 2 copies of a row give the same result as 0 (or 4, 6, etc). And even without multiple copies of rows, you can force any hash you'd like by observing what happens when you insert more random rows and finding a subcollection that flips exactly the bits you want.

What you probably want to look at is homomorphic hashing. This is usually implemented by hashing each row to an element of an appropriate abelian group and then using the group operation to combine them.

With suitable choice of group, this hash can have cryptographic strength. Some interesting choices here are lattices (LtHash), elliptic curves (ECMH), multiplicative groups (MuHash).

Sometimes these are officially sanctioned and even required! Most notably, including logos/other embellishments are a form of "trap street" where the idea is to have something to point to that trivially proves someone is using your mask design if it comes to it.

The usual next difficulty is that the maximum shebang length is fairly low (truncated at 128 chars, IIRC)

My understanding is that was the original purpose, but probably unnecessary given that all the relevant process steps are encased in tools that are not exposed to the general clean room environment in operation (they have to maintain a higher grade of clean room internally).

However, I suspect it's probably going to continue being propagated forward due to Copy Exactly which has historically meant that Intel documents and copies the smallest details in all their fabs just in case they are necessary. In the end, if it ain't broke...

If I wanted to keep the blur aesthetic, I'd probably do a full removal, run an inpainting algorithm to replace the removed region with something less jarring in context and then blur the result. The inpainting algorithm can be fairly low quality and still get acceptable results since it won't be seen directly.

As Izkata mentions, the superproject has _all_ the files for a given commit without any need for users to have access other repos, additional submodule init commands, etc.

Basically, after a subrepo clone, you've copied the file tree for the subrepo and can make commits on it in the superproject to your heart's content (branching, etc). This is basically a fork/mirror, but adds a single metadata file to track the last upstream commit you pushed/pulled from to allow reconciling later. So with git subrepo, you make commits in the superproject first and can choose (at some later point, if at all) to merge with the subrepo upstream. This is arguably consistent with the git model writ large (make local commits, later choose if/how to integrate those with upstream). Importantly, people that clone your superproject repo don't have to know anything about subrepo or special commands to send changes back to you.

For submodules, changes flow in the other direction. If you want to make a change to the child repo, you must 1) commit in the submodule, 2) push the submodule commit to its upstream, 3) make a commit in the super project that changes the commit the submodule is pointing to. When someone pulls, switches branches, etc in the superproject, they need to do a submodule update with various failure modes or else they end up with empty/out-of-date content.

Subtrees are a bit similar to subrepos, but in practice you still need to be aware of their boundaries since you can't mix subtree/superproject modifications in the same commit. Moreover, you need to use a special merge strategy rather than git default merge/rebase which subrepo uses.

Note that the time taken is linear with respect to the original execution.

A cycle of n instructions starting at instruction n0 will be detected in between n0 and n0+n iterations (i.e. <= 3*(n0+n) underlying instructions) since n0 iterations gets both into the cycle and the offset between them will become 0 some time in the next n iterations.

n could be very large, of course (e.g, using all of memory as a giant counter so the cycle length is huge), but the cycle detection is not really making your problem worse.

There's no need to store all previous states to detect a cycle: it can be done using just twice the original memory.

You can model the state transitions as a linked list and use Floyd's classical tortoise and hare algorithm to (eventually) determine a cycle exists. Initialize "tortoise" and "hare" as two copies of initial state and advance hare by two instructions and tortoise by one each iteration. A cycle is reported if the two states become equal again.

I've had success using \import{subdir/}{BasenameInSubdir} from the import package.

The basic (and unfortunate in a xkcd/1479 way) issue appears to be that the arXiv compile server doesn't allow writing to subdirectories. A subdir \include implicitly requires write access for the aux file.

That's certainly been my experience.

I've had arXiv automatically block bare uploads of TeX-derived PDFs (presumably identified through PDF metadata). For these, it required that the source be uploaded and compiled on their server.

On balance, it's probably best to require source as arXiv does, but this can create interesting issues from time to time. Since the source is downloadable, researchers can inadvertently end up sharing partial results or snark that was commented out in the TeX source.