100 hypotheses + jailbreak fork

Z / Runner 🏃🏻‍♂️

🏃🏻‍♂️ re: LLM/SMT (knowledge w/ integrity); are you planning to introduce formal logic systems into ai(s)? I see the value that LLMs are not supposed to be the oracle (facts/figures/solvers), so combining SMT may improve the ability for some aspect of creative/information outputs.

🏃🏻‍♂️ Manus and I suspect gemini3/gpt5 doesn't try to reason their way through compute heavy prompts (we can see that w/ manus as it exposes its virtue sandbox -- generating a series of python scripts and executes it on a virtualized ubuntu instance). I assume w/ ai(s), we can integrate beyond python/shell scripts and include top excel macros / fxs.

• 🏃🏻‍♂️ ah, i was thinking abstracting the actual fx calls & scripting just as manus. Meaning, net/net the users are not interfacing w/ the scripts even at the prompt level.

• 🏃🏻‍♂️ "Variables represent concepts in your Automated Reasoning policy that can have values assigned to them when translating natural language into formal logic. Your policy rules define constraints on what are valid or invalid values for these variables."... this is the "iffy" part, sounds good on paper and assume LLMs can accurately automate this process.

• 🏃🏻‍♂️ grounding the facts via RAG, i see most LLMs & tooling kits are capable of directly linking outputs w/ the underlying vector db (i.e. referencing the source material). This works well for knowledge retrieval, documents, or any data types that are small (less than 10ish). But i haven't seen any good techniques on how to visualize vector db.

• 🏃🏻‍♂️ grounding = directly referencing source; visualizing = transform data into new coordinate/dimension (e.g. plotting, but doesn't always mean charting/graphing). The latter is more useful for the messy middle

• 🏃🏻‍♂️ It is a hard problem when vector embeddings are usually high on dimensions. Excel does this well b/c it can rely on charts and graphs for (2-3 dimensional data), and for medium size, users rely on pivot table for open exploration or use macros to programmatically compress. Have you seen any good solutions? In the world of R, there are many stat packages that can automate the data.

• 🏃🏻‍♂️ good point, these are 2 different problems. I want to explore how to improve language embedding. As for proof trees, I think it is a much harder problem to solve – don't know much about it, as you previously shared mathematical reasoning (lean).

• 🏃🏻‍♂️ let me try below: Circling around a real world problem: messy middle = most of the (information/knowledge/data/facts) are not purely symbolic logic or ambiguous language (wording, terms, phrases, statements). Is it safe to assume that we can't force a homogenous system? How do you keep 2 distinctively different representations (related yes) alive and run compute on top of it? Another way of saying it, hard logic vs. soft logic.

• 🏃🏻‍♂️ yes, but you can see this explodes into nth degree when it comes to problems are the stateful.

• 🏃🏻‍♂️ will digg deeper, to be fair, aaron & I both shared similar experiences that manus isn't all that smart when it comes to cleanly sort thru provided context. Hence I use manus for workflow automation, never deep analysis. You also witness how many errors manus made during basic ETL (fx health pdf to spreadsheet).

• 🏃🏻‍♂️ (formal logic vs. loosey reasoning per language). A subset of problem: numerical data and facts are meaningless w/o soft and messy context. Clear example is the magnesium chat, the types, dose is so messy and specific to the "state". Meaning, real-world data isn't high-dimensional globally, it is local. To be fair, application specific models are trying to address this by grounding the outputs w/ direct link.

• 🏃🏻‍♂️ precise states is the messy part. Mixed data types is no longer the challenge, it is conditional validity. So I agree w/ you context-engineering is probably the best solution we have at the moment.

• 🏃🏻‍♂️ Embrace uncertainty: how do you enumerate qualifiers? Can systems track epistemic "unknowns". For example, many of my biomarkers are graded across confidence internals, have competing hypotheses, assumptions on limited context. Hence, i think why you also get frustrated w/ conflicting suggestions. This is where i have doubts on how can SMT fail gracefully (LLMs will probably just hallunciate or use ambiguous wording to mask the problem).

• 🏃🏻‍♂️ if i were to rank: use LLMs to compress high-dimensional data, expose variables that can be useful for symbolic systems (SMT) to enforce hard logic (stating the obvious/obvious). Then replicate what manus has already proofed, shell tooling to handle data transformation, ai(s); w/ key diff & improvement on human-in the loop context gating. This is where i feel the pain when using manus, i can see within the sandbox where their system is going down the wrong path, but I have no way to directly manipulate the "messy middle".

• 🏃🏻‍♂️ Trying to explain this: manus like all LLMs, assume a flat, linear reasoning/compute path. Ideally, most of us know there are hierarchical representations and forks within/around the embedding. Maybe, what I call the messy middle = latent (hidden) space, where coarse to fine, general to specific still need direct user inputs (ie. similar to how excel data manipulation works).

• 🏃🏻‍♂️ I keep using the pivot table example, this is how analyst explore and find hidden meaning (or stories) in the olden days… where the users can intercept the calculator midstreams and add their own "context" why certain data needs to be compressed, grouped, calculated. Stating the obv/obv; in excel this is very limited b/c people choke on combinatorial explosions or just too lazy to run high-volume of exploration. But w/ assisted prompting, this maybe a solvable problem. I guess it is tool augmented reasoning on top of execution paths. This is probably what you see w/ solvers and why manus is so graceful when it comes to information manipulation.

Stephen / Basketball 🏀

• 🏀 per "predefined checks" today and "neuro-symbolic" below.

• 🏀 great for: self consistency (integrity), debate scoring (rewards), resolve conflicts (constraints), fit schedules (minimalization).

• 🏀 ha, not even "=ai(..)" but "=textbefore(..)" in the top 10. and, "vba code to google".

• 🏀 yup, manus specifically says shell as the general compute.

• 🏀 per "world champion" below!

• 🏀 already deployed, see "Automated Reasoning Checks" below.

• 🏀 yes, hence imo gold medalist: auto-formalization + de-formalization.

• 🏀 what's the difference between grounding vs visualizing vector embeddings?

• 🏀 you are conflating language embedding (vector) vs proof trees (logic) vs data understanding (stats)?

• 🏀 you sure it's about embedding? let's work through a concrete example together. see "task types" on the google api: semantic_similarity, classification, clustering, retrieval_query , code_retrieval_query, question_answering, fact_verification.

• 🏀 such as: which supplements to take?

• 🏀 hence, context engineering is the key / solution.

• 🏀 no doubt. hence, my expertise: finding the json for the lab results – bingo, 100% accuracy.

• 🏀 which 2 representations? examples, examples!

• 🏀 yup, i asked for the confidence intervals, impact %, ranked predictions.

• 🏀 nothing soft or messy about it, just more / precise states in the context.

• 🏀 oh, we want probabilistic reasoning.

• 🏀 definitely not about (data) dimension reduction or compression. see "checkpoints + backtracks" below today.

• 🏀 yes, spreadsheet is still far more interactive, being able to visualize / manipulation exploration paths, and guiding directions / results. see "co (human + agent)" below.

• 🏀 i see your analogy now: analysts on spreadsheet use endless data, tables, tabs.. to explore then =join() to merge. yes, same in deepmind's alpha*, lean theorem proving, .. actually, manus' checkpoints is not only very limited but for long-horizontal completion: hence, hours-long tasks with 100 steps and wide research on 100 links – but not yet, exploring and merging 100 hypotheses.

• 🏀 "Manus's brain turns into goldfish memory with a chainsaw."

🏀 (minimal) fork any product via url. leaked 10 months ago via jailbreak prompt by jian liao at agentbase (as acknowledged).

🏀 bechnmarks: meta's general ai assistants 2 (gaia2), meta's agents research environments (are), scale ai's remote labor index (rli).

• "what are the most valuable use cases of ai agents doing days-long tasks in 2026?"

• upwork's future index, stanford's human index, mit's iceberg index

• swe bench, web arena, os world, app world, spider sql

• mit's encompass search tree as checkpoints + backtracks for code migration / refactor / optimization / release: upgrade toolschains + packages, then diff screenshots of web pages + mobile flows.

• co (human + agent): 30 vs 70% completion, but human alone takes 29 hours on average; audit with predefined checks and cross-page reference.