Understanding an AI-generated proof in theoretical computer science may soon be like trying to understand the assembly code produced by an optimizing C compiler. It's technically possible, but why spend time doing it when better tools can do the work for you?

Instead of having theoretical computer scientists spend weeks or months checking AI-generated proofs and trying to extract insights from them, we should publish these proofs with formal verification in Lean.

Each paper would contain an English writeup and a corresponding Lean formalization. Lean would verify the formal proof, while future generations of increasingly powerful AIs would:

• Check that the English statements accurately correspond to their Lean formalizations.
• Find mistakes or discrepancies that earlier AIs missed.
• Simplify the arguments and discover more elegant proofs.
• Extract insights about algorithms, complexity, computational models, and other theoretical concepts, then explain them to researchers in simple English.
• Generalize the results and discover connections to other areas of theoretical computer science.

The papers could be continuously improved as stronger AIs become available, while preserving earlier versions.

Given how quickly AI capabilities are improving, a theoretical computer scientist might spend six months understanding a complicated proof that an AI released a year later could explain clearly in minutes.

Why not leave that work to future AIs?

Human researchers could focus on identifying interesting computational problems, exploring applications, and developing new research directions. They could still benefit from the insights contained in AI-generated proofs without having to decipher the proofs themselves.

The goal should be to advance theoretical computer science and make its proof insights automatically accessible to humans via ever more powerful AIs.

Hi all,

Hopefully not asking a silly question: which practical applications of CS would you highlight in the context of having passed the test of time?

This question came to my mind while talking with colleagues about the impact and longevity of TCP/IP (obviouslly with changes and improvements over time, but essentially TCP/IP still today)

In the case of programming languages, C and "LISP" come to my mind (even though nowadays they might not be so much in active use, their influence, for good or bad, can be felt everywhere)

Now that LLM is almost ubiquous in discussions, a candidate could also be Neural Networks.

I am curious also about failure stories - sometimes much more can be learned from a theory or application that proved wrong (against the initial promises)

Thanks!

Hi all,

I'd like to share some recent work in stringology / text mining. We developed BloomSpan, an algorithm for mining Maximal Contiguous Frequent Phrases (MCFPs) from large text corpora — token sequences that occur in at least σ documents and can't be extended on either side without dropping below σ. Unlike general Sequential Pattern Mining (GSP, PrefixSpan, BIDE+), no gaps are allowed, which matters for things like template extraction, plagiarism detection and phrase mining, where gaps only blow up the candidate space.

How it works

To be fair, it's less a brand-new algorithm than a careful combination of known pieces:

• A Counting Bloom Filter for probabilistic n-gram frequency estimation. Seed filtering is provably free of false negatives — the CBF can only over-estimate counts.
• Prioritized depth-first expansion directly on the corpus, with no recursive projected databases.
• A global occupancy bitmask plus an inverted index keyed on each pattern's rarest token, for maximality checks and redundancy control.

Memory stays O(W + M) in the input size (corpus + filter).

Results

• On Gutenberg-BookCorpus-Cleaned (up to 50k books, ~3.07B tokens, σ = 20): 11–15× faster wall-clock than FHK (Fischer–Heun–Kramer) with up to 2x lower peak memory. It's the only algorithm we tested that completes the 3B-token subset within a 40 GB heap.
• Output is identical to exact baselines (FHK, DFI) on every Gutenberg-8k subset where a baseline finishes.
• On synthetic data with flat frequency distributions or dense nested overlaps, FHK's LCP-interval traversal wins.

The paper includes a topological analysis (LZ phrase ratio / entropy rate) of why natural language is the sweet spot.

Links

• Preprint: https://www.researchgate.net/publication/415565702_BloomSpan_Memory-Efficient_Maximal_Frequent_Substring_Mining_for_Large-Scale_Text
• Code (Java, C++): https://github.com/raliev/bloomspan

Happy to discuss implementation details, data structure choices, or the dataset topology analysis.

Hello, I want to share a project that i've been working on for the last month or so. It's and implementation (from what i could find the only rn on the internet) of Andreas Bjorklund's theoretical algorithm for determining weather a graph is hamiltonian or not. The algorithm is revolutionary because it lowered the exponential part of the time complexity of Held-Karp which is the standard algorithm for determining weather a graph is hamiltonian, from O^*(2n) to O^*(1.657n) for general graphs(this is what i've managed to implement as of right not) and for bipartite its O^*(1.414n).

It might have some logical errors, and could maybe be optimised but right now, as of writting this it is 4AM and i want to sleep.

link to paper: https://arxiv.org/pdf/1008.0541

link to the github repo: https://github.com/Ak0-m/Bjorklunds_algorithm_for_Hamiltonicity

I've been going deep on data structures lately and found bloom filters pretty intriguing. I made a short video on what a bloom filter is, how the bit array and hash functions interact, and where the false positive formula comes from.

link: https://youtu.be/nNv4ZTQp_s8?si=j52fIUBYaDcaps0_

I'd love feedback, especially if I got anything wrong. Happy to go through the derivation in the comments if anyone wants it.

So, lean is the language built specifically to prove theorems.but if the algorithm will be rewritten in another programming language, such as python, will it be accepted?

(mathematical theorems)

Main Website: https://www.ruleflow.org/

For the past year, I have been developing a framework to simulate certain discrete systems for a research team at my university (paid for by the School of Engineering and Physics, but I had the freedom to license it under MIT). As it turns out, I got carried away generalizing it to work for many, many different types of complex systems (String Rewriting Systems, Cellular Automata, etc.) and ended up creating our own domain-specific language.

The website's landing page has a bunch of GIF-style examples... so you should be able to get a good idea of what this project is about.

If any of y'all are interested in this, feel free to take a look and try it out!

EDIT:

Out of the interest of not being "vague", here are some more details. RuleFlow was developed with a primary focus on analyzing causality in Sequential Substitution Systems. This is why there is a major focus on causal graphs, cellular identity, etc. While originally developed for Sequential Sub Systems, we generalized the DSL to support many types of rewriting systems by providing the user with flags and directives to control how rules behave. Furthermore, we bootstrapped Python and the Wolfram Language so that complex rulesets could be scaffolded as macros. The main goal of RuleFlow is NOT simply to simulate systems (there's already plenty of software for that, such as Golly and even just Mathematica), but to provide extensive tooling for causal analysis.

Here is some interesting research from our (small) team:

• An Improved Generalized Enumeration of Substitution Systems by Kenneth E. Caviness, Camille Morrow, Christen Case and Victoria Kratzke
• Indexed Concatenation Notation: A Novel Way to Summarize Networks and Other Complex Systems

My job has been to provide better research tooling, extending what we already have in Mathematica code to open source and free Python.

Some video games, many of them are retro, are based on tiles. They have different levels which may be huge and logically highly complex but they are all based on limited sets of tiles.
Even a minute long video is usually bigger in file size than the retrog game itself.
It happens with Prince of Persia, Boulder Dash, Supaplex, Commander Keen, Bio Menace etc. - easier to recognize in two-dimensional games.
If video encoding used a database of tiles available in the game, it would enable much smaller file sizes and also higher quality of video as it would not have to use approximations to reduce file size as the tiles are exactly the same everywhere (meaning that lossless video would be affordable by bitrate). I am under no pressure to get it implemented ASAP but I would like a technological discussion about how-to.

Here's the idea: we source and collect interesting computational puzzles, then we send them out to participants who have a month to work on them and send in their solutions. At the end of every month, we meet and discuss how the problems went and where people got stuck, what approaches they took, and any extensions people came up with.

Thoughts?
.
.
.
.
If you're curious, here's a taste of what a representative sample problem might look like:

Given the coordinates of an arbitrary polygon (e.g. irregular and/or non-convex), how might you implement a program to efficiently sample a point uniformly from its interior?

TIP: If using the Python programming language, you can check out the shapely library.
Bonus: what if there are holes?

(Please don't spoil the problem, it's searchable anyways.)

I am currently reading Complexity: A Guided Tour by Melanie Mitchell and since it was published in 2009, I am wondering if there are more “modern”/“up-to-date” intro books.

So I am in 2nd year of college and after exploring here and there and there, I am genuinely interested in systems programming, I know c, ofcourse I will learn it deeply but what do I learn after it

The whole thing feels very overwhelming,

What shall be the flow of learning

Been thinking about memory management in languages without a GC, and there's an approach I hadn't really seen before that I'm curious how people feel about compared to Rust.

In this model you can allocate objects as much as you like, pass objects around and put them in collections, all without lifetimes or moves. Nothing is ever freed automatically, not even at end of the scope. If you want the memory back you write free obj; yourself, and the compiler has to prove nobody else can still see it. If it can't prove that, it won't compile. Same for use after free and double free.

The Ironwood language does it this way. It's compiled with a closed-world link, so the compiler sees the whole program when it checks those frees. There's also defer free x; for cleanup on exceptions. If you just never call free, the memory stays allocated and you get a warning. Fine for a CLI tool, not so fine for a server.

The appeal is that you only have to prove anything at the point where you free. The rest of the code doesn't care. The downside is you have to remember to free.

Rust gets you automatic drops and a stronger guarantee overall, but you're thinking about ownership on every line, which at least for me is counter-productive.

Which memory management approach would you rather work with? And why?

```java // Ironwood: does NOT compile

public class Garage {

private static class Engine {

    void start() {
        System.out.println("Vroom!");
    }
}

private static class Car {

    private final Engine engine;

    Car(Engine engine) {
        this.engine = engine; // the car keeps a reference to the engine
    }

    void drive() {
        engine.start();
    }
}

public static void main(String[] args) {

    Engine engine = new Engine();
    Car car = new Car(engine);

    // Compiler error: the car still holds a reference to the engine,
    // so freeing it here would leave car.engine dangling.
    //
    //   error: cannot free 'engine': allocation is still borrowed by a live wrapper
    //
    // Fix: free the car first, then the engine.
    free engine;

    car.drive(); // would use a freed engine
    free car;
}

} ```

```rust // Rust: does NOT compile

struct Engine;

impl Engine { fn start(&self) { println!("Vroom!"); } }

// The car keeps a reference to the engine, so it needs a lifetime parameter. struct Car<'a> { engine: &'a Engine, }

impl<'a> Car<'a> { fn drive(&self) { self.engine.start(); } }

fn main() { let engine = Engine; let car = Car { engine: &engine };

// Compiler error: the car still borrows the engine,
// so dropping it here would leave car.engine dangling.
//
//   error[E0505]: cannot move out of `engine` because it is borrowed
//
// Fix: remove the drop and let both go out of scope
// (car is dropped before engine automatically).
drop(engine);

car.drive(); // would use a dropped engine

} ```

Has somebody ever understood or is educated enough to understand a computer from top to bottom. Meaning knowing a deep undergraduate level knowledge of math & physics -> computer science -> electrical engineering/computer engineering as if having all 4 degrees. If someone is knowledgeable in this or tried to study something similar like this, what is your experience? Will this knowledge help you become more skilled? What will you gain from studying this?

Hi! Im considering a masters thesis about compression of large amounts of data for long-term archival. But instead of trying to revolutionize all of compression, i want to focus on a few, narrow domains, which are however still useful to people.