feat: add HOL4 tests and update NEUROSYM.scm with v2 radial network spec

- Add 12 unit tests for HOL4 prover backend
  - Parser tests: simple term, numeral, application, lambda, forall, exists
  - Type tests: bool, num, arrow (function type)
  - Backend tests: creation, config, term conversion
- Fix type mismatches using correct HOL4Type variants (TyCon, TyFun)
- Update NEUROSYM.scm to v2.0.0 with radial network architecture spec
  - Document RBFN for similarity-based proof acceleration
  - Include similarity matching, prover integration, axiom theory alignment
  - Add workflow, challenges, and ECHIDNA-specific integration notes

Test results: 114 unit tests, 38 integration tests all passing

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: Jonathan D.A. Jewell

.machine_readable/NEUROSYM.scm

@@ -1,13 +1,85 @@
 ;; SPDX-License-Identifier: AGPL-3.0-or-later
-;; NEUROSYM.scm - Neurosymbolic integration config for echidna
+;; NEUROSYM.scm - Neurosymbolic integration config for ECHIDNA
 
 (define neurosym-config
-  `((version . "1.0.0")
+  `((version . "2.0.0")
+
+    ;; Current implementation (v1): GNN + Transformer
     (symbolic-layer
       ((type . "scheme")
        (reasoning . "deductive")
        (verification . "formal")))
+
     (neural-layer
-      ((embeddings . false)
-       (fine-tuning . false)))
-    (integration . ())))
+      ((architecture . "gnn-transformer")
+       (embeddings . true)
+       (fine-tuning . false)
+       (prover-encoders . ("agda" "coq" "lean" "isabelle" "z3" "cvc5"
+                           "metamath" "hol-light" "mizar" "pvs" "acl2" "hol4"))))
+
+    (integration
+      ((rust-julia-api . "http")
+       (api-port . 8081)
+       (caching . true)
+       (diversity-ranking . true)))
+
+    ;; v2 Planned: Radial Basis Function Network Integration
+    (v2-radial-network
+      ((status . "planned")
+       (description . "RBFN for similarity-based proof acceleration")
+
+       ;; Core concept: Radial networks (RBFNs) for similarity matching
+       (similarity-matching
+         ((feature-extraction . "Encode proofs, theorems, problem states as vectors using embeddings from proof terms, syntax trees, or semantic graphs")
+          (similarity-metric . "Gaussian kernel radial basis functions to measure similarity between new problems and solved proofs/axioms")
+          (clustering . "Group similar proofs/problem states for efficient axiom retrieval")))
+
+       ;; Integration with multi-prover system
+       (prover-integration
+         ;; A. Preprocessing: Axiom/Proof Embedding
+         ((embedding-layer . "Convert axioms, lemmas, proof steps to shared vector space via GNN for syntax trees or transformers for proof scripts")
+          (radial-basis . "Train RBFN on embeddings to map similar proofs/theorems to nearby regions")
+
+          ;; B. Real-Time Acceleration
+          (query-matching . "Embed new problem state and query RBFN for most similar axioms/proof fragments")
+          (proof-guidance . (
+            "Prune search spaces (SAT solvers, tableau methods)"
+            "Suggest relevant lemmas (Lean4/Coq tactics)"
+            "Prioritize solver strategies based on historical success"))
+
+          ;; C. Dynamic Learning
+          (feedback-loop . "Update RBFN with new embeddings as solver proves theorems")
+          (active-learning . "Focus on regions where solver struggles")))
+
+       ;; Axiom theory alignment
+       (axiom-theory
+         ((axiom-selection . "Prioritize frequently-used axioms from similar proofs")
+          (hierarchical-abstraction . "Abstract over low-level proof steps for higher-level reasoning")
+          (consistency-checks . "Cross-validate retrieved axioms against problem's logical context")))
+
+       ;; Implementation architecture
+       (architecture
+         ((symbolic-core . "Handles formal logic and verification via prover backends")
+          (neural-accelerator . "RBFN guides search, reduces redundant computations")
+          (database-backend . "Graph database for embeddings (ArangoDB/Virtuoso)")
+          (approximate-nn . "FAISS/Annoy for scalable nearest-neighbor search")))
+
+       ;; Workflow
+       (workflow
+         ("1. Input: New conjecture from any of 12 provers"
+          "2. Embed: Convert conjecture and context to vector"
+          "3. Retrieve: RBFN returns similar proofs/axioms from database"
+          "4. Solve: Solver uses hints to construct proof, fallback to exhaustive search"
+          "5. Update: Add new proof embedding to RBFN"))
+
+       ;; Challenges
+       (challenges
+         ((soundness . "Ensure suggestions are logically valid via formal verification")
+          (scalability . "Use approximate NN for large proof corpora")
+          (interpretability . "Visualize similarity space with UMAP/t-SNE")))
+
+       ;; ECHIDNA-specific integration
+       (echidna-integration
+         ((tree-of-thought . "RBFN acts as subsequent selector for proof tree exploration")
+          (anti-tampering . "Hash embeddings with SHAKE-256 for proof integrity")
+          (proactive-suggestions . "Preemptively suggest optimizations based on proof patterns")))))))

src/rust/provers/hol4.rs

@@ -2115,3 +2115,143 @@ impl ProverBackend for Hol4Backend {
         self.config = config;
     }
 }
+
+// ============================================================================
+// Tests
+// ============================================================================
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_parse_simple_term() {
+        let mut parser = HOL4Parser::new("x");
+        let term = parser.parse_term().unwrap();
+        match term {
+            HOL4Term::Var { name, .. } => assert_eq!(name, "x"),
+            _ => panic!("Expected variable"),
+        }
+    }
+
+    #[test]
+    fn test_parse_numeral() {
+        let mut parser = HOL4Parser::new("42");
+        let term = parser.parse_term().unwrap();
+        assert_eq!(term, HOL4Term::Numeral(42));
+    }
+
+    #[test]
+    fn test_parse_application() {
+        let mut parser = HOL4Parser::new("f x");
+        let term = parser.parse_term().unwrap();
+        match term {
+            HOL4Term::App { func, arg } => {
+                match *func {
+                    HOL4Term::Var { name, .. } => assert_eq!(name, "f"),
+                    _ => panic!("Expected function variable"),
+                }
+                match *arg {
+                    HOL4Term::Var { name, .. } => assert_eq!(name, "x"),
+                    _ => panic!("Expected argument variable"),
+                }
+            }
+            _ => panic!("Expected application"),
+        }
+    }
+
+    #[test]
+    fn test_parse_lambda() {
+        let mut parser = HOL4Parser::new("\\x. x");
+        let term = parser.parse_term().unwrap();
+        match term {
+            HOL4Term::Abs { var, body, .. } => {
+                assert_eq!(var, "x");
+                match *body {
+                    HOL4Term::Var { name, .. } => assert_eq!(name, "x"),
+                    _ => panic!("Expected variable in body"),
+                }
+            }
+            _ => panic!("Expected lambda abstraction"),
+        }
+    }
+
+    #[test]
+    fn test_parse_forall() {
+        let mut parser = HOL4Parser::new("!x. P x");
+        let term = parser.parse_term().unwrap();
+        match term {
+            HOL4Term::Quant { quantifier, var, .. } => {
+                assert_eq!(quantifier, HOL4Quantifier::Forall);
+                assert_eq!(var, "x");
+            }
+            _ => panic!("Expected forall quantification"),
+        }
+    }
+
+    #[test]
+    fn test_parse_exists() {
+        let mut parser = HOL4Parser::new("?x. P x");
+        let term = parser.parse_term().unwrap();
+        match term {
+            HOL4Term::Quant { quantifier, var, .. } => {
+                assert_eq!(quantifier, HOL4Quantifier::Exists);
+                assert_eq!(var, "x");
+            }
+            _ => panic!("Expected exists quantification"),
+        }
+    }
+
+    #[test]
+    fn test_parse_type_bool() {
+        let mut parser = HOL4Parser::new("bool");
+        let ty = parser.parse_type().unwrap();
+        assert_eq!(ty, HOL4Type::TyCon("bool".to_string()));
+    }
+
+    #[test]
+    fn test_parse_type_num() {
+        let mut parser = HOL4Parser::new("num");
+        let ty = parser.parse_type().unwrap();
+        assert_eq!(ty, HOL4Type::TyCon("num".to_string()));
+    }
+
+    #[test]
+    fn test_parse_type_arrow() {
+        let mut parser = HOL4Parser::new("num -> bool");
+        let ty = parser.parse_type().unwrap();
+        match ty {
+            HOL4Type::TyFun { domain, range } => {
+                assert_eq!(*domain, HOL4Type::TyCon("num".to_string()));
+                assert_eq!(*range, HOL4Type::TyCon("bool".to_string()));
+            }
+            _ => panic!("Expected function type"),
+        }
+    }
+
+    #[test]
+    fn test_term_to_universal() {
+        let term = HOL4Term::Numeral(42);
+        let universal = Hol4Backend::hol4_to_term(&term);
+        match universal {
+            Term::Const(name) => assert_eq!(name, "42"),
+            _ => panic!("Expected constant"),
+        }
+    }
+
+    #[test]
+    fn test_hol4_backend_creation() {
+        let backend = Hol4Backend::new(ProverConfig::default());
+        assert_eq!(backend.kind(), ProverKind::HOL4);
+    }
+
+    #[test]
+    fn test_hol4_config() {
+        let config = ProverConfig {
+            executable: PathBuf::from("/usr/bin/hol4"),
+            ..Default::default()
+        };
+        let backend = Hol4Backend::new(config);
+        assert_eq!(backend.config().executable, PathBuf::from("/usr/bin/hol4"));
+    }
+}