{"id":"W3022975118","doi":"","title":"SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics","year":2018,"lang":"en","type":"article","venue":"arXiv (Cornell University)","topic":"Polynomial and algebraic computation","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Wilfrid Laurier University; University of Waterloo","funders":"","keywords":"Mathematical proof; Pruning; Automated theorem proving; Computer science; Domain (mathematical analysis); Variety (cybernetics); Theoretical computer science; Mathematics; Artificial intelligence","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006905307,0.001409889,0.001881802,0.003629506,0.002247187,0.0111323,0.002506689,0.003989785,0.01421607],"category_scores_gemma":[0.01466866,0.001508786,0.001957601,0.003354018,0.01449181,0.02977337,0.008556506,0.01473459,0.004653939],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002328021,"about_ca_system_score_gemma":0.002585614,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001381312,"about_ca_topic_score_gemma":0.001623885,"domain_scores_codex":[0.9916052,0.004079836,0.0004410495,0.001045956,0.002455528,0.000372444],"domain_scores_gemma":[0.9859006,0.0107546,0.0003347783,0.001872525,0.0006867099,0.000450819],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.00002403756,0.00001796256,0.0001571715,0.0002232731,0.00002936063,0.00006903985,0.000261009,0.001035891,0.0003179849,0.9592103,0.007398628,0.03125538],"study_design_scores_gemma":[0.0000162022,0.00001715898,0.00009194607,0.0001920291,0.00001188151,0.0001328904,0.00008622103,0.004026835,0.0002321786,0.9258808,0.06928661,0.00002528008],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.007611919,0.1013962,0.6429355,0.111887,0.003606891,0.0001481896,0.0004735193,0.00229059,0.1296503],"genre_scores_gemma":[0.2301784,0.09641236,0.604035,0.02541966,0.01487111,0.0006075656,0.001109165,0.001297691,0.02606915],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01421607,"threshold_uncertainty_score":0.04755747,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03470944831623364,"score_gpt":0.1777916292314339,"score_spread":0.1430821809152003,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}